overlay hott and odd-order

Author: Tragicus

dev/ci/user-overlays/19611-tragicus-evarconv-save-keys.sh

@@ -1 +1,2 @@
-overlay mathcomp https://github.com/tragicus/math-comp weak-cs 19611
+overlay odd-order https://github.com/tragicus/odd-order pr19611 19611
+overlay Coq-HoTT https://github.com/Tragicus/Coq-HoTT pr19611 19611

pretyping/evarconv.mli

@@ -95,10 +95,10 @@ val apply_hooks : hook
 exception No_cs of bool
 
 val decompose_proj : env -> evar_map -> state -> (Names.Constant.t * EConstr.EInstance.t) *
-            (EConstr.t list * EConstr.t * Reductionops.Stack.t)
+            (EConstr.t list option * EConstr.t * Reductionops.Stack.t)
 val check_conv_record : env -> evar_map ->
   (Names.Constant.t * EConstr.EInstance.t) *
-            (EConstr.t list * EConstr.t * Reductionops.Stack.t) ->
+            (EConstr.t list option * EConstr.t * Reductionops.Stack.t) ->
   state ->
   evar_map * (constr * constr)
   * constr * constr list * (EConstr.t list * EConstr.t list option) *