Moving Evd.evars_of_term from constr to econstr + consequences.

This impacts a lot of code, apparently in the good, removing several
conversions back and forth constr.

12 files changed, 41 insertions, 48 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index be0318fbde..6888526f5b 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -657,7 +657,7 @@ let clear_hyps2_in_evi env sigma hyps t concl ids =
 let queue_set q is_dependent set =
   Evar.Set.iter (fun a -> Queue.push (is_dependent,a) q) set
 let queue_term q is_dependent c =
-  queue_set q is_dependent (evars_of_term (EConstr.Unsafe.to_constr c))
+  queue_set q is_dependent (evars_of_term c)
 
 let process_dependent_evar q acc evm is_dependent e =
   let evi = Evd.find evm e in
@@ -675,7 +675,7 @@ let process_dependent_evar q acc evm is_dependent e =
   | Evar_empty ->
       if is_dependent then Evar.Map.add e None acc else acc
   | Evar_defined b ->
-      let subevars = evars_of_term (EConstr.Unsafe.to_constr b) in
+      let subevars = evars_of_term b in
       (* evars appearing in the definition of an evar [e] are marked
          as dependent when [e] is dependent itself: if [e] is a
          non-dependent goal, then, unless they are reach from another
@@ -795,7 +795,7 @@ let filtered_undefined_evars_of_evar_info ?cache sigma evi =
   in
   let accu = match evi.evar_body with
   | Evar_empty -> Evar.Set.empty
-  | Evar_defined b -> evars_of_term (EConstr.Unsafe.to_constr b)
+  | Evar_defined b -> evars_of_term b
   in
   let accu = Evar.Set.union (undefined_evars_of_term sigma evi.evar_concl) accu in
   let ctxt = EConstr.Unsafe.to_named_context (evar_filtered_context evi) in
diff --git a/engine/evd.mli b/engine/evd.mli
index 29235050b0..3cb4031f11 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -495,7 +495,7 @@ val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t option
     contained in the object; need the term to be evar-normal otherwise
     defined evars are returned too. *)
 
-val evars_of_term : constr -> Evar.Set.t
+val evars_of_term : econstr -> Evar.Set.t
   (** including evars in instances of evars *)
 
 val evars_of_named_context : (econstr, etypes) Context.Named.pt -> Evar.Set.t
diff --git a/engine/proofview.ml b/engine/proofview.ml
index ecea637947..b77839c28e 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -1253,7 +1253,7 @@ module V82 = struct
 
   let top_evars initial =
     let evars_of_initial (c,_) =
-      Evar.Set.elements (Evd.evars_of_term (EConstr.Unsafe.to_constr c))
+      Evar.Set.elements (Evd.evars_of_term c)
     in
     CList.flatten (CList.map evars_of_initial initial)
 
diff --git a/engine/termops.ml b/engine/termops.ml
index 8a6bd17948..67fc8edf6e 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -187,7 +187,7 @@ let compute_evar_dependency_graph sigma =
     in
     match evar_body evi with
     | Evar_empty -> acc
-    | Evar_defined c -> Evar.Set.fold fold_ev (evars_of_term (EConstr.Unsafe.to_constr c)) acc
+    | Evar_defined c -> Evar.Set.fold fold_ev (evars_of_term c) acc
   in
   Evd.fold fold sigma EvMap.empty
 
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index 075ebf006a..57a068f82a 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -290,7 +290,7 @@ let finalize_view s0 ?(simple_types=true) p =
 Goal.enter_one ~__LOC__ begin fun g ->
   let env = Goal.env g in
   let sigma = Goal.sigma g in
-  let evars_of_p = Evd.evars_of_term (EConstr.to_constr ~abort_on_undefined_evars:false sigma p) in
+  let evars_of_p = Evd.evars_of_term p in
   let filter x _ = Evar.Set.mem x evars_of_p in
   let sigma = Typeclasses.resolve_typeclasses ~fail:false ~filter env sigma in
   let p = Reductionops.nf_evar sigma p in
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 4e0866a0c5..e421b31227 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -544,7 +544,7 @@ let dont_impact_evars_in cl =
 (*  - w_unify expands let-in (zeta conversion) eagerly, whereas we want to  *)
 (*    match a head let rigidly.                                             *)
 let match_upats_FO upats env sigma0 ise orig_c =
-  let dont_impact_evars = dont_impact_evars_in orig_c in
+  let dont_impact_evars = dont_impact_evars_in (EConstr.of_constr orig_c) in
   let rec loop c =
     let f, a = splay_app ise c in let i0 = ref (-1) in
     let fpats =
@@ -586,7 +586,7 @@ let match_upats_FO upats env sigma0 ise orig_c =
 
 
 let match_upats_HO ~on_instance upats env sigma0 ise c =
- let dont_impact_evars = dont_impact_evars_in c in
+ let dont_impact_evars = dont_impact_evars_in (EConstr.of_constr c) in
  let it_did_match = ref false in
  let failed_because_of_TC = ref false in
  let rec aux upats env sigma0 ise c =
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index 2b32838964..74a3ee035c 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -41,7 +41,7 @@ let simple_goal sigma g gs =
   let open Evd in
   let open Evarutil in
   let evi = Evd.find sigma g in
-  Set.is_empty (evars_of_term (EConstr.Unsafe.to_constr evi.evar_concl)) &&
+  Set.is_empty (evars_of_term evi.evar_concl) &&
   Set.is_empty (evars_of_filtered_evar_info (nf_evar_info sigma evi)) &&
   not (List.exists (Proofview.depends_on sigma g) gs)
 
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 9f233a2551..ece9fc8937 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -374,6 +374,7 @@ let declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~po
     let obls, constr, typ =
       match term with
       | Some t ->
+        let termtype = EConstr.of_constr termtype in
         let obls, _, constr, typ =
           Obligations.eterm_obligations env id sigma 0 t termtype
         in obls, Some constr, typ
@@ -400,7 +401,7 @@ let declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~po
           if not (Option.is_empty term) then
             let init_refine =
               Tacticals.New.tclTHENLIST [
-                Refine.refine ~typecheck:false (fun sigma -> (sigma,EConstr.of_constr (Option.get term)));
+                Refine.refine ~typecheck:false (fun sigma -> (sigma, Option.get term));
                 Proofview.Unsafe.tclNEWGOALS (CList.map Proofview.with_empty_state gls);
                 Tactics.New.reduce_after_refine;
               ]
@@ -497,10 +498,10 @@ let do_instance ~pstate env env' sigma ?hook ~refine ~tac ~global ~poly ~program
   (* Check that the type is free of evars now. *)
   Pretyping.check_evars env (Evd.from_env env) sigma termtype;
   let termtype = to_constr sigma termtype in
-  let term = Option.map (to_constr ~abort_on_undefined_evars:false sigma) term in
   let pstate =
     if not (Evd.has_undefined sigma) && not (Option.is_empty props) then
-      (declare_instance_constant k pri global imps ?hook id decl poly sigma (Option.get term) termtype;
+      let term = to_constr sigma (Option.get term) in
+      (declare_instance_constant k pri global imps ?hook id decl poly sigma term termtype;
        None)
     else if program_mode || refine || Option.is_empty props then
       declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl (List.map RelDecl.get_name ctx) term termtype
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 12df3215ad..d2c986fe5c 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -88,11 +88,12 @@ let do_definition ~ontop ~program_mode ?hook ident k univdecl bl red_option c ct
     let (c,ctx), sideff = Future.force ce.const_entry_body in
     assert(Safe_typing.empty_private_constants = sideff);
     assert(Univ.ContextSet.is_empty ctx);
+    Obligations.check_evars env evd;
+    let c = EConstr.of_constr c in
     let typ = match ce.const_entry_type with
-      | Some t -> t
-      | None -> EConstr.to_constr ~abort_on_undefined_evars:false evd (Retyping.get_type_of env evd (EConstr.of_constr c))
+      | Some t -> EConstr.of_constr t
+      | None -> Retyping.get_type_of env evd c
     in
-    Obligations.check_evars env evd;
     let obls, _, c, cty =
       Obligations.eterm_obligations env ident evd 0 c typ
     in
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 20a2db7ca2..3befdc5885 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -230,12 +230,9 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
   in
   (* XXX: Capturing sigma here... bad bad *)
   let hook = Lemmas.mk_hook (hook sigma) in
-  (* XXX: Grounding non-ground terms here... bad bad *)
-  let fullcoqc = EConstr.to_constr ~abort_on_undefined_evars:false sigma def in
-  let fullctyp = EConstr.to_constr ~abort_on_undefined_evars:false sigma typ in
   Obligations.check_evars env sigma;
   let evars, _, evars_def, evars_typ =
-    Obligations.eterm_obligations env recname sigma 0 fullcoqc fullctyp
+    Obligations.eterm_obligations env recname sigma 0 def typ
   in
   let ctx = Evd.evar_universe_context sigma in
     ignore(Obligations.add_definition recname ~term:evars_def ~univdecl:decl
@@ -262,17 +259,13 @@ let do_program_recursive local poly fixkind fixl ntns =
   let evd = nf_evar_map_undefined evd in
   let collect_evars id def typ imps =
     (* Generalize by the recursive prototypes  *)
-    let def =
-      EConstr.to_constr ~abort_on_undefined_evars:false evd (Termops.it_mkNamedLambda_or_LetIn def rec_sign)
-    and typ =
-      (* Worrying... *)
-      EConstr.to_constr ~abort_on_undefined_evars:false evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign)
-    in
+    let def = nf_evar evd (Termops.it_mkNamedLambda_or_LetIn def rec_sign) in
+    let typ = nf_evar evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign) in
     let evm = collect_evars_of_term evd def typ in
     let evars, _, def, typ =
       Obligations.eterm_obligations env id evm
-        (List.length rec_sign) def typ
-    in (id, def, typ, imps, evars)
+        (List.length rec_sign) def typ in
+    (id, def, typ, imps, evars)
   in
   let (fixnames,fixrs,fixdefs,fixtypes) = fix in
   let fiximps = List.map pi2 info in
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 1b1c618dc7..771ae2053f 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -39,7 +39,7 @@ let check_evars env evm =
 
 type oblinfo =
   { ev_name: int * Id.t;
-    ev_hyps: Constr.named_context;
+    ev_hyps: EConstr.named_context;
     ev_status: bool * Evar_kinds.obligation_definition_status;
     ev_chop: int option;
     ev_src: Evar_kinds.t Loc.located;
@@ -50,11 +50,11 @@ type oblinfo =
 (** Substitute evar references in t using de Bruijn indices,
   where n binders were passed through. *)
 
-let subst_evar_constr evs n idf t =
+let subst_evar_constr evm evs n idf t =
   let seen = ref Int.Set.empty in
   let transparent = ref Id.Set.empty in
   let evar_info id = List.assoc_f Evar.equal id evs in
-  let rec substrec (depth, fixrels) c = match Constr.kind c with
+  let rec substrec (depth, fixrels) c = match EConstr.kind evm c with
     | Evar (k, args) ->
 	let { ev_name = (id, idstr) ;
 	      ev_hyps = hyps ; ev_chop = chop } =
@@ -84,18 +84,18 @@ let subst_evar_constr evs n idf t =
 	  in aux hyps args []
 	in
 	  if List.exists
-            (fun x -> match Constr.kind x with
+            (fun x -> match EConstr.kind evm x with
             | Rel n -> Int.List.mem n fixrels
             | _ -> false) args
           then
 	    transparent := Id.Set.add idstr !transparent;
-	  mkApp (idf idstr, Array.of_list args)
+          EConstr.mkApp (idf idstr, Array.of_list args)
     | Fix _ ->
-	Constr.map_with_binders succfix substrec (depth, 1 :: fixrels) c
-    | _ -> Constr.map_with_binders succfix substrec (depth, fixrels) c
+        EConstr.map_with_binders evm succfix substrec (depth, 1 :: fixrels) c
+    | _ -> EConstr.map_with_binders evm succfix substrec (depth, fixrels) c
   in
   let t' = substrec (0, []) t in
-    t', !seen, !transparent
+    EConstr.to_constr evm t', !seen, !transparent
 
 
 (** Substitute variable references in t using de Bruijn indices,
@@ -112,18 +112,18 @@ let subst_vars acc n t =
     to a product : forall H1 : t1, ..., forall Hn : tn, concl.
     Changes evars and hypothesis references to variable references.
 *)
-let etype_of_evar evs hyps concl =
+let etype_of_evar evm evs hyps concl =
   let open Context.Named.Declaration in
   let rec aux acc n = function
       decl :: tl ->
-	let t', s, trans = subst_evar_constr evs n mkVar (NamedDecl.get_type decl) in
+        let t', s, trans = subst_evar_constr evm evs n EConstr.mkVar (NamedDecl.get_type decl) in
 	let t'' = subst_vars acc 0 t' in
 	let rest, s', trans' = aux (NamedDecl.get_id decl :: acc) (succ n) tl in
 	let s' = Int.Set.union s s' in
 	let trans' = Id.Set.union trans trans' in
 	  (match decl with
             | LocalDef (id,c,_) ->
-		let c', s'', trans'' = subst_evar_constr evs n mkVar c in
+                let c', s'', trans'' = subst_evar_constr evm evs n EConstr.mkVar c in
 		let c' = subst_vars acc 0 c' in
                   mkNamedProd_or_LetIn (LocalDef (id, c', t'')) rest,
 		Int.Set.union s'' s',
@@ -131,7 +131,7 @@ let etype_of_evar evs hyps concl =
             | LocalAssum (id,_) ->
                 mkNamedProd_or_LetIn (LocalAssum (id, t'')) rest, s', trans')
     | [] ->
-	let t', s, trans = subst_evar_constr evs n mkVar concl in
+        let t', s, trans = subst_evar_constr evm evs n EConstr.mkVar concl in
 	  subst_vars acc 0 t', s, trans
   in aux [] 0 (List.rev hyps)
 
@@ -209,9 +209,7 @@ let eterm_obligations env name evm fs ?status t ty =
       (fun (id, (n, nstr), ev) l ->
 	 let hyps = Evd.evar_filtered_context ev in
          let hyps = trunc_named_context nc_len hyps in
-         let hyps = EConstr.Unsafe.to_named_context hyps in
-         let concl = EConstr.Unsafe.to_constr ev.evar_concl in
-         let evtyp, deps, transp = etype_of_evar l hyps concl in
+         let evtyp, deps, transp = etype_of_evar evm l hyps ev.evar_concl in
 	 let evtyp, hyps, chop =
 	   match chop_product fs evtyp with
 	   | Some t -> t, trunc_named_context fs hyps, fs
@@ -237,9 +235,9 @@ let eterm_obligations env name evm fs ?status t ty =
       evn []
   in
   let t', _, transparent = (* Substitute evar refs in the term by variables *)
-    subst_evar_constr evts 0 mkVar t 
+    subst_evar_constr evm evts 0 EConstr.mkVar t
   in
-  let ty, _, _ = subst_evar_constr evts 0 mkVar ty in
+  let ty, _, _ = subst_evar_constr evm evts 0 EConstr.mkVar ty in
   let evars = 
     List.map (fun (ev, info) ->
       let { ev_name = (_, name); ev_status = force_status, status;
@@ -252,7 +250,7 @@ let eterm_obligations env name evm fs ?status t ty =
       in name, typ, src, (force_status, status), deps, tac) evts
   in
   let evnames = List.map (fun (ev, info) -> ev, snd info.ev_name) evts in
-  let evmap f c = pi1 (subst_evar_constr evts 0 f c) in
+  let evmap f c = pi1 (subst_evar_constr evm evts 0 f c) in
     Array.of_list (List.rev evars), (evnames, evmap), t', ty
 
 let hide_obligation () =
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index d25daeed9c..9214ddd4b9 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -26,14 +26,14 @@ val sort_dependencies : (Evar.t * evar_info * Evar.Set.t) list -> (Evar.t * evar
 (* env, id, evars, number of function prototypes to try to clear from
    evars contexts, object and type *)
 val eterm_obligations : env -> Id.t -> evar_map -> int ->
-  ?status:Evar_kinds.obligation_definition_status -> constr -> types ->
+  ?status:Evar_kinds.obligation_definition_status -> EConstr.constr -> EConstr.types ->
   (Id.t * types * Evar_kinds.t Loc.located *
      (bool * Evar_kinds.obligation_definition_status) * Int.Set.t *
       unit Proofview.tactic option) array
     (* Existential key, obl. name, type as product, 
        location of the original evar, associated tactic,
        status and dependencies as indexes into the array *)
-  * ((Evar.t * Id.t) list * ((Id.t -> constr) -> constr -> constr)) *
+  * ((Evar.t * Id.t) list * ((Id.t -> EConstr.constr) -> EConstr.constr -> constr)) *
     constr * types
     (* Translations from existential identifiers to obligation identifiers 
        and for terms with existentials to closed terms, given a