Leminv API using EConstr.

4 files changed, 12 insertions, 8 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index c2ad3c462..35fe9cf66 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -68,6 +68,9 @@ let rec flush_and_check_evars sigma c =
        | Some c -> flush_and_check_evars sigma c)
   | _ -> map_constr (flush_and_check_evars sigma) c
 
+let flush_and_check_evars sigma c =
+  flush_and_check_evars sigma (EConstr.Unsafe.to_constr c)
+
 (* let nf_evar_key = Profile.declare_profile "nf_evar"  *)
 (* let nf_evar = Profile.profile2 nf_evar_key Reductionops.nf_evar *)
 
@@ -474,12 +477,13 @@ let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ?nami
 (* This assumes an evar with identity instance and generalizes it over only
    the De Bruijn part of the context *)
 let generalize_evar_over_rels sigma (ev,args) =
+  let open EConstr in
   let evi = Evd.find sigma ev in
   let sign = named_context_of_val evi.evar_hyps in
   List.fold_left2
     (fun (c,inst as x) a d ->
-      if isRel a then (mkNamedProd_or_LetIn d c,a::inst) else x)
-     (evi.evar_concl,[]) (Array.to_list args) sign
+      if isRel sigma a then (mkNamedProd_or_LetIn d c,a::inst) else x)
+     (EConstr.of_constr evi.evar_concl,[]) (Array.to_list args) sign
 
 (************************************)
 (* Removing a dependency in an evar *)
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 82346b24e..ad3851ea3 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -170,7 +170,7 @@ val nf_evar_map_universes : evar_map -> evar_map * (constr -> constr)
 
 (** Replacing all evars, possibly raising [Uninstantiated_evar] *)
 exception Uninstantiated_evar of existential_key
-val flush_and_check_evars :  evar_map -> constr -> constr
+val flush_and_check_evars :  evar_map -> EConstr.constr -> constr
 
 (** {6 Term manipulation up to instantiation} *)
 
@@ -220,7 +220,7 @@ val push_rel_decl_to_named_context :
 val push_rel_context_to_named_context : Environ.env -> EConstr.types ->
   named_context_val * EConstr.types * EConstr.constr list * csubst * (identifier*EConstr.constr) list
 
-val generalize_evar_over_rels : evar_map -> existential -> types * constr list
+val generalize_evar_over_rels : evar_map -> EConstr.existential -> EConstr.types * EConstr.constr list
 
 (** Evar combinators *)
 
diff --git a/engine/termops.ml b/engine/termops.ml
index 4ab9f0733..ef7cdc38b 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -233,9 +233,9 @@ let it_named_context_quantifier f ~init =
 let it_mkProd_or_LetIn init = it_named_context_quantifier mkProd_or_LetIn ~init
 let it_mkProd_wo_LetIn init = it_named_context_quantifier mkProd_wo_LetIn ~init
 let it_mkLambda_or_LetIn init = it_named_context_quantifier mkLambda_or_LetIn ~init
-let it_mkNamedProd_or_LetIn init = it_named_context_quantifier mkNamedProd_or_LetIn ~init
+let it_mkNamedProd_or_LetIn init = it_named_context_quantifier EConstr.mkNamedProd_or_LetIn ~init
 let it_mkNamedProd_wo_LetIn init = it_named_context_quantifier mkNamedProd_wo_LetIn ~init
-let it_mkNamedLambda_or_LetIn init = it_named_context_quantifier mkNamedLambda_or_LetIn ~init
+let it_mkNamedLambda_or_LetIn init = it_named_context_quantifier EConstr.mkNamedLambda_or_LetIn ~init
 
 let it_mkLambda_or_LetIn_from_no_LetIn c decls =
   let open RelDecl in
diff --git a/engine/termops.mli b/engine/termops.mli
index 1c14e6c89..72c0cedda 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -51,9 +51,9 @@ val it_mkLambda : EConstr.constr -> (Name.t * EConstr.types) list -> EConstr.con
 val it_mkProd_or_LetIn : types -> Context.Rel.t -> types
 val it_mkProd_wo_LetIn : EConstr.types -> Context.Rel.t -> EConstr.types
 val it_mkLambda_or_LetIn : constr -> Context.Rel.t -> constr
-val it_mkNamedProd_or_LetIn : types -> Context.Named.t -> types
+val it_mkNamedProd_or_LetIn : EConstr.types -> Context.Named.t -> EConstr.types
 val it_mkNamedProd_wo_LetIn : types -> Context.Named.t -> types
-val it_mkNamedLambda_or_LetIn : constr -> Context.Named.t -> constr
+val it_mkNamedLambda_or_LetIn : EConstr.constr -> Context.Named.t -> EConstr.constr
 
 (* Ad hoc version reinserting letin, assuming the body is defined in
    the context where the letins are expanded *)