Equality API using EConstr.

6 files changed, 18 insertions, 15 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 9e0a55a0df..1dd9d0c005 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -78,6 +78,8 @@ type cofixpoint = (t, t) pcofixpoint
 type unsafe_judgment = (constr, types) Environ.punsafe_judgment
 type unsafe_type_judgment = types Environ.punsafe_type_judgment
 
+let in_punivs a = (a, Univ.Instance.empty)
+
 let mkProp = of_kind (Sort Sorts.prop)
 let mkSet = of_kind (Sort Sorts.set)
 let mkType u = of_kind (Sort (Sorts.Type u))
@@ -92,8 +94,11 @@ let mkLambda (na, t, c) = of_kind (Lambda (na, t, c))
 let mkLetIn (na, b, t, c) = of_kind (LetIn (na, b, t, c))
 let mkApp (f, arg) = of_kind (App (f, arg))
 let mkConstU pc = of_kind (Const pc)
+let mkConst c = of_kind (Const (in_punivs c))
 let mkIndU pi = of_kind (Ind pi)
+let mkInd i = of_kind (Ind (in_punivs i))
 let mkConstructU pc = of_kind (Construct pc)
+let mkConstruct c = of_kind (Construct (in_punivs c))
 let mkCase (ci, c, r, p) = of_kind (Case (ci, c, r, p))
 let mkFix f = of_kind (Fix f)
 let mkCoFix f = of_kind (CoFix f)
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 15463a8f68..e6270fa78f 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -62,12 +62,12 @@ val mkProd : Name.t * t * t -> t
 val mkLambda : Name.t * t * t -> t
 val mkLetIn : Name.t * t * t * t -> t
 val mkApp : t * t array -> t
-(* val mkConst : constant -> t *)
+val mkConst : constant -> t
 val mkConstU : pconstant -> t
 val mkProj : (projection * t) -> t
-(* val mkInd : inductive -> t *)
+val mkInd : inductive -> t
 val mkIndU : pinductive -> t
-(* val mkConstruct : constructor -> t *)
+val mkConstruct : constructor -> t
 val mkConstructU : pconstructor -> t
 (* val mkConstructUi : pinductive * int -> t *)
 val mkCase : case_info * t * t * t array -> t
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 4f40499d0a..c2ad3c4628 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -690,29 +690,26 @@ let rec advance sigma evk =
 
 let undefined_evars_of_term evd t =
   let rec evrec acc c =
-    match kind_of_term c with
+    match EConstr.kind evd c with
       | Evar (n, l) ->
-	let acc = Array.fold_left evrec acc l in
-	(try match (Evd.find evd n).evar_body with
-	  | Evar_empty -> Evar.Set.add n acc
-	  | Evar_defined c -> evrec acc c
-	 with Not_found -> anomaly ~label:"undefined_evars_of_term" (Pp.str "evar not found"))
-      | _ -> fold_constr evrec acc c
+        let acc = Evar.Set.add n acc in
+	Array.fold_left evrec acc l
+      | _ -> EConstr.fold evd evrec acc c
   in
   evrec Evar.Set.empty t
 
 let undefined_evars_of_named_context evd nc =
   Context.Named.fold_outside
-    (NamedDecl.fold_constr (fun c s -> Evar.Set.union s (undefined_evars_of_term evd c)))
+    (NamedDecl.fold_constr (fun c s -> Evar.Set.union s (undefined_evars_of_term evd (EConstr.of_constr c))))
     nc
     ~init:Evar.Set.empty
 
 let undefined_evars_of_evar_info evd evi =
-  Evar.Set.union (undefined_evars_of_term evd evi.evar_concl)
+  Evar.Set.union (undefined_evars_of_term evd (EConstr.of_constr evi.evar_concl))
     (Evar.Set.union
        (match evi.evar_body with
 	 | Evar_empty -> Evar.Set.empty
-	 | Evar_defined b -> undefined_evars_of_term evd b)
+	 | Evar_defined b -> undefined_evars_of_term evd (EConstr.of_constr b))
        (undefined_evars_of_named_context evd
 	  (named_context_of_val evi.evar_hyps)))
 
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 6620bbaed2..82346b24e2 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -121,7 +121,7 @@ val advance : evar_map -> evar -> evar option
     This is roughly a combination of the previous functions and
     [nf_evar]. *)
 
-val undefined_evars_of_term : evar_map -> constr -> Evar.Set.t
+val undefined_evars_of_term : evar_map -> EConstr.constr -> Evar.Set.t
 val undefined_evars_of_named_context : evar_map -> Context.Named.t -> Evar.Set.t
 val undefined_evars_of_evar_info : evar_map -> evar_info -> Evar.Set.t
 
diff --git a/engine/termops.ml b/engine/termops.ml
index b7932665a4..c2d862f005 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -1074,7 +1074,7 @@ let global_vars_set env sigma constr =
   let rec filtrec acc c =
     let acc = match EConstr.kind sigma c with
     | Var _ | Const _ | Ind _ | Construct _ ->
-      Id.Set.union (vars_of_global env (EConstr.Unsafe.to_constr c)) acc
+      Id.Set.union (vars_of_global env (EConstr.to_constr sigma c)) acc
     | _ -> acc
     in
     EConstr.fold sigma filtrec acc c
diff --git a/engine/termops.mli b/engine/termops.mli
index 7758a57eee..013efcbcb3 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -256,6 +256,7 @@ val compact_named_context : Context.Named.t -> Context.Compacted.t
 val clear_named_body : Id.t -> env -> env
 
 val global_vars : env -> Evd.evar_map -> EConstr.t -> Id.t list
+val global_vars_set : env -> Evd.evar_map -> EConstr.t -> Id.Set.t
 val global_vars_set_of_decl : env -> Evd.evar_map -> Context.Named.Declaration.t -> Id.Set.t
 val global_app_of_constr : Evd.evar_map -> EConstr.constr -> Globnames.global_reference puniverses * EConstr.constr option