evarconf transp state and comments fixes

2 files changed, 20 insertions, 19 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index f1845af7f2..cfa0875ca5 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -190,7 +190,7 @@ let occur_rigidly flags env evd (evk,_) t =
     | Ind _ | Sort _ -> Rigid false
     | Proj (p, c) ->
       let cst = Projection.constant p in
-      let rigid = not (is_transparent_constant flags.open_ts cst) in
+      let rigid = not (TransparentState.is_transparent_constant flags.open_ts cst) in
         if rigid then aux c
         else (* if the evar appears rigidly in c then this elimination
                 cannot reduce and we have a rigid occurrence, otherwise
@@ -208,7 +208,7 @@ let occur_rigidly flags env evd (evk,_) t =
     | Lambda (na, t, b) -> aux b
     | LetIn (na, _, _, b) -> aux b
     | Const (c,_) ->
-      if is_transparent_constant flags.open_ts c then Reducible
+      if TransparentState.is_transparent_constant flags.open_ts c then Reducible
       else Rigid false
     | Prod (_, b, t) ->
       let b' = aux b and t' = aux t in
@@ -789,7 +789,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
         and f3 i = miller true (sp1,al1) appr1 appr2 i
         and f4 i = miller false (sp2,al2) appr2 appr1 i
         and f5 i =
-          (** We ensure failure of consuming the stacks does not
+          (* We ensure failure of consuming the stacks does not
              propagate an error about unification of the stacks while
              the heads themselves cannot be unified, so we return
              NotSameHead. *)
@@ -934,7 +934,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
 	     let c = nf_evar i c1 in
              let na = Nameops.Name.pick na1 na2 in
              evar_conv_x flags (push_rel (RelDecl.LocalAssum (na,c)) env) i CONV c'1 c'2);
-           (** When in modulo_betaiota = false case, lambda's are not reduced *)
+           (* When in modulo_betaiota = false case, lambda's are not reduced *)
            (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk1 sk2)]
 
     | Flexible ev1, Rigid -> flex_rigid true ev1 appr1 appr2
@@ -1014,7 +1014,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
         | Int _, Int _ ->
           rigids env evd sk1 term1 sk2 term2
 
-        | Evar (sp1,al1), Evar (sp2,al2) -> (** Frozen evars *)
+        | Evar (sp1,al1), Evar (sp2,al2) -> (* Frozen evars *)
           if Evar.equal sp1 sp2 then
             match ise_stack2 false env evd (evar_conv_x flags) sk1 sk2 with
             |None, Success i' ->
@@ -1341,7 +1341,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
   let instance = List.map mkVar vars in
   let rhs = nf_evar evd rhs in
   if not (noccur_evar env_rhs evd evk rhs) then raise (TypingFailed evd);
-  (** Ensure that any progress made by Typing.e_solve_evars will not contradict
+  (* Ensure that any progress made by Typing.e_solve_evars will not contradict
       the solution we are trying to build here by adding the problem as a constraint. *)
   let evd = Evarutil.add_unification_pb (CONV,env_rhs,mkEvar (evk,args),rhs) evd in
   let prc env evd c = Termops.Internal.print_constr_env env evd c in
@@ -1393,9 +1393,9 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
                                    str" of type: " ++ prc env_evar evd evty ++
                                    str " for " ++ prc env_rhs evd c);
           let instance = Filter.filter_list filter instance in
-          (** Allow any type lower than the variable's type as the
-              abstracted subterm might have a smaller type, which could be
-              crucial to make the surrounding context typecheck. *)
+          (* Allow any type lower than the variable's type as the
+             abstracted subterm might have a smaller type, which could be
+             crucial to make the surrounding context typecheck. *)
           let evd, evty =
             if isArity evd evty then
               refresh_universes ~status:Evd.univ_flexible (Some true)
@@ -1419,12 +1419,12 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
 
   let evd, rhs' = set_holes env_rhs evd rhs subst in
   let rhs' = nf_evar evd rhs' in
-  (** Thin evars making the term typable in env_evar *)
+  (* Thin evars making the term typable in env_evar *)
   let evd, rhs' = thin_evars env_evar evd ctxt rhs' in
   (* We instantiate the evars of which the value is forced by typing *)
   if !debug_ho_unification then
     (Feedback.msg_debug Pp.(str"solve_evars on: " ++ prc env_evar evd rhs');
-     Feedback.msg_debug Pp.(str"evars: " ++ pr_evar_map (Some 0) evd));
+     Feedback.msg_debug Pp.(str"evars: " ++ pr_evar_map (Some 0) env_evar evd));
   let evd,rhs' =
     try !solve_evars env_evar evd rhs'
     with e when Pretype_errors.precatchable_exception e ->
@@ -1434,7 +1434,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
   (* We instantiate the evars of which the value is forced by typing *)
   if !debug_ho_unification then
     (Feedback.msg_debug Pp.(str"after solve_evars: " ++ prc env_evar evd rhs');
-     Feedback.msg_debug Pp.(str"evars: " ++ pr_evar_map (Some 0) evd));
+     Feedback.msg_debug Pp.(str"evars: " ++ pr_evar_map (Some 0) env_evar evd));
 
   let rec abstract_free_holes evd = function
    | (id,idty,c,cty,evsref,_,_)::l ->
@@ -1483,7 +1483,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
      in force_instantiation evd !evsref
    | [] ->
      if Evd.is_defined evd evk then
-       (** Can happen due to dependencies: instantiating evars in the arguments of evk might
+       (* Can happen due to dependencies: instantiating evars in the arguments of evk might
            instantiate evk itself. *)
        (if !debug_ho_unification then
           begin
@@ -1501,7 +1501,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
            if !debug_ho_unification then
              Feedback.msg_debug Pp.(str"abstracted type before second solve_evars: " ++
                                       prc evenv evd rhs');
-         (** solve_evars is not commuting with nf_evar, because restricting
+         (* solve_evars is not commuting with nf_evar, because restricting
              an evar might provide a more specific type. *)
           let evd, _ = !solve_evars evenv evd rhs' in
           if !debug_ho_unification then
@@ -1591,7 +1591,7 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 =
      let f flags ontype env evd pbty x y =
        let reds =
          match ontype with
-         | TypeUnification -> full_transparent_state
+         | TypeUnification -> TransparentState.full
          | TermUnification -> flags.open_ts
        in is_fconv ~reds pbty env evd x y
      in
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 2c4a2f144e..0fe47c2a48 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -19,7 +19,7 @@ open Locus
 type unify_flags = Evarsolve.unify_flags
 
 (** The default subterm transparent state is no unfoldings *)
-val default_flags_of : ?subterm_ts:transparent_state -> transparent_state -> unify_flags
+val default_flags_of : ?subterm_ts:TransparentState.t -> TransparentState.t -> unify_flags
 
 type unify_fun = unify_flags ->
   env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result
@@ -36,7 +36,7 @@ exception UnableToUnify of evar_map * Pretype_errors.unification_error
 
 (** Theses functions allow to pass arbitrary flags to the unifier and can delay constraints.
     In case the flags are not specified, they default to
-    [default_flags_of full_transparent_state] currently.
+    [default_flags_of TransparentState.full] currently.
 
     In case of success, the two terms are hence unifiable only if the remaining constraints
     can be solved or [check_problems_are_solved] is true.
@@ -53,9 +53,10 @@ val the_conv_x_leq : env -> ?ts:TransparentState.t -> constr -> constr -> evar_m
 [@@ocaml.deprecated "Use Evarconv.unify_leq_delay instead"]
 (** The same function resolving evars by side-effect and
    catching the exception *)
-val conv : env -> ?ts:transparent_state -> evar_map -> constr -> constr -> evar_map option
+
+val conv : env -> ?ts:TransparentState.t -> evar_map -> constr -> constr -> evar_map option
 [@@ocaml.deprecated "Use Evarconv.unify_delay instead"]
-val cumul : env -> ?ts:transparent_state -> evar_map -> constr -> constr -> evar_map option
+val cumul : env -> ?ts:TransparentState.t -> evar_map -> constr -> constr -> evar_map option
 [@@ocaml.deprecated "Use Evarconv.unify_leq_delay instead"]
 
 (** This function also calls [solve_unif_constraints_with_heuristics] to resolve any remaining