Evar-normalizing functions now act on EConstrs.

5 files changed, 35 insertions, 34 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 8940be09d..42620c0b5 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -99,16 +99,21 @@ let rec whd_evar sigma c =
 	if u' == u then c else mkConstructU (co, u')
     | _ -> c
 
-let rec nf_evar sigma t = Constr.map (fun t -> nf_evar sigma t) (whd_evar sigma t)
-let e_nf_evar sigma t = EConstr.of_constr (nf_evar sigma (EConstr.Unsafe.to_constr t))
+(** Term exploration up to instantiation. *)
+let kind_of_term_upto sigma t =
+  Constr.kind (whd_evar sigma t)
+
+let rec nf_evar0 sigma t = Constr.map (fun t -> nf_evar0 sigma t) (whd_evar sigma t)
+let whd_evar sigma c = EConstr.of_constr (whd_evar sigma (EConstr.Unsafe.to_constr c))
+let nf_evar sigma c = EConstr.of_constr (nf_evar0 sigma (EConstr.Unsafe.to_constr c))
 
 let j_nf_evar sigma j =
-  { uj_val = e_nf_evar sigma j.uj_val;
-    uj_type = e_nf_evar sigma j.uj_type }
+  { uj_val = nf_evar sigma j.uj_val;
+    uj_type = nf_evar sigma j.uj_type }
 let jl_nf_evar sigma jl = List.map (j_nf_evar sigma) jl
 let jv_nf_evar sigma = Array.map (j_nf_evar sigma)
 let tj_nf_evar sigma {utj_val=v;utj_type=t} =
-  {utj_val=e_nf_evar sigma v;utj_type=t}
+  {utj_val=nf_evar sigma v;utj_type=t}
 
 let nf_evars_universes evm =
   Universes.nf_evars_and_universes_opt_subst (safe_evar_value evm) 
@@ -125,23 +130,23 @@ let e_nf_evars_and_universes evdref =
 let nf_evar_map_universes evm =
   let evm = Evd.nf_constraints evm in
   let subst = Evd.universe_subst evm in
-    if Univ.LMap.is_empty subst then evm, nf_evar evm
+    if Univ.LMap.is_empty subst then evm, nf_evar0 evm
     else
       let f = nf_evars_universes evm in
 	Evd.raw_map (fun _ -> map_evar_info f) evm, f
 
 let nf_named_context_evar sigma ctx =
-  Context.Named.map (nf_evar sigma) ctx
+  Context.Named.map (nf_evar0 sigma) ctx
 
 let nf_rel_context_evar sigma ctx =
-  Context.Rel.map (nf_evar sigma) ctx
+  Context.Rel.map (nf_evar0 sigma) ctx
 
 let nf_env_evar sigma env =
   let nc' = nf_named_context_evar sigma (Environ.named_context env) in
   let rel' = nf_rel_context_evar sigma (Environ.rel_context env) in
     push_rel_context rel' (reset_with_named_context (val_of_named_context nc') env)
 
-let nf_evar_info evc info = map_evar_info (nf_evar evc) info
+let nf_evar_info evc info = map_evar_info (nf_evar0 evc) info
 
 let nf_evar_map evm =
   Evd.raw_map (fun _ evi -> nf_evar_info evm evi) evm
@@ -527,7 +532,7 @@ let rec check_and_clear_in_constr env evdref err ids global c =
       | Evar (evk,l as ev) ->
 	  if Evd.is_defined !evdref evk then
 	    (* If evk is already defined we replace it by its definition *)
-	    let nc = whd_evar !evdref c in
+	    let nc = Evd.existential_value !evdref ev in
 	      (check_and_clear_in_constr env evdref err ids global nc)
 	  else
 	    (* We check for dependencies to elements of ids in the
@@ -582,7 +587,7 @@ let rec check_and_clear_in_constr env evdref err ids global c =
 	      let evi' = { evi with evar_extra = extra' } in
 	      evdref := Evd.add !evdref evk evi' ;
 	    (* spiwack: /hacking session *)
-              whd_evar !evdref c
+              Evd.existential_value !evdref ev
 
       | _ -> map_constr (check_and_clear_in_constr env evdref err ids global) c
 
@@ -751,10 +756,6 @@ let subterm_source evk (loc,k) =
   (loc,Evar_kinds.SubEvar evk)
 
 
-(** Term exploration up to instantiation. *)
-let kind_of_term_upto sigma t =
-  Constr.kind (whd_evar sigma t)
-
 (** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and
     [u] up to existential variable instantiation and equalisable
     universes. The term [t] is interpreted in [sigma1] while [u] is
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index ea9599c8b..67de18abc 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -139,8 +139,8 @@ val judge_of_new_Type : 'r Sigma.t -> (unsafe_judgment, 'r) Sigma.sigma
 (** [flush_and_check_evars] raise [Uninstantiated_evar] if an evar remains
     uninstantiated; [nf_evar] leaves uninstantiated evars as is *)
 
-val whd_evar :  evar_map -> constr -> constr
-val nf_evar :  evar_map -> constr -> constr
+val whd_evar :  evar_map -> EConstr.constr -> EConstr.constr
+val nf_evar :  evar_map -> EConstr.constr -> EConstr.constr
 val j_nf_evar :  evar_map -> EConstr.unsafe_judgment -> EConstr.unsafe_judgment
 val jl_nf_evar :
    evar_map -> EConstr.unsafe_judgment list -> EConstr.unsafe_judgment list
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 9e5e9c7da..ab72cc405 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -24,7 +24,7 @@ type proofview = Proofview_monad.proofview
 
 (* The first items in pairs below are proofs (under construction).
    The second items in the pairs below are statements that are being proved. *)
-type entry = (Term.constr * Term.types) list
+type entry = (EConstr.constr * EConstr.types) list
 
 (** Returns a stylised view of a proofview for use by, for instance,
     ide-s. *)
@@ -37,15 +37,16 @@ let proofview p =
   p.comb , p.solution
 
 let compact el ({ solution } as pv) =
-  let nf = Evarutil.nf_evar solution in
+  let nf c = Evarutil.nf_evar solution c in
+  let nf0 c = EConstr.Unsafe.to_constr (Evarutil.nf_evar solution (EConstr.of_constr c)) in
   let size = Evd.fold (fun _ _ i -> i+1) solution 0 in
   let new_el = List.map (fun (t,ty) -> nf t, nf ty) el in
   let pruned_solution = Evd.drop_all_defined solution in
   let apply_subst_einfo _ ei =
     Evd.({ ei with
-       evar_concl =  nf ei.evar_concl;
-       evar_hyps = Environ.map_named_val nf ei.evar_hyps;
-       evar_candidates = Option.map (List.map nf) ei.evar_candidates }) in
+       evar_concl =  nf0 ei.evar_concl;
+       evar_hyps = Environ.map_named_val nf0 ei.evar_hyps;
+       evar_candidates = Option.map (List.map nf0) ei.evar_candidates }) in
   let new_solution = Evd.raw_map_undefined apply_subst_einfo pruned_solution in
   let new_size = Evd.fold (fun _ _ i -> i+1) new_solution 0 in
   Feedback.msg_info (Pp.str (Printf.sprintf "Evars: %d -> %d\n" size new_size));
@@ -56,7 +57,7 @@ let compact el ({ solution } as pv) =
 
 type telescope =
   | TNil of Evd.evar_map
-  | TCons of Environ.env * Evd.evar_map * Term.types * (Evd.evar_map -> Term.constr -> telescope)
+  | TCons of Environ.env * Evd.evar_map * EConstr.types * (Evd.evar_map -> EConstr.constr -> telescope)
 
 let typeclass_resolvable = Evd.Store.field ()
 
@@ -71,11 +72,10 @@ let dependent_init =
   | TNil sigma -> [], { solution = sigma; comb = []; shelf = [] }
   | TCons (env, sigma, typ, t) ->
     let sigma = Sigma.Unsafe.of_evar_map sigma in
-    let Sigma (econstr, sigma, _) = Evarutil.new_evar env sigma ~src ~store (EConstr.of_constr typ) in
-    let econstr = EConstr.Unsafe.to_constr econstr in
+    let Sigma (econstr, sigma, _) = Evarutil.new_evar env sigma ~src ~store typ in
+    let (gl, _) = EConstr.destEvar (Sigma.to_evar_map sigma) econstr in
     let sigma = Sigma.to_evar_map sigma in
     let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in
-    let (gl, _) = Term.destEvar econstr in
     let entry = (econstr, typ) :: ret in
     entry, { solution = sol; comb = gl :: comb; shelf = [] }
   in
@@ -1222,12 +1222,12 @@ module V82 = struct
    { Evd.it = comb ; sigma = solution }
 
   let top_goals initial { solution=solution; } =
-    let goals = CList.map (fun (t,_) -> fst (Term.destEvar t)) initial in
+    let goals = CList.map (fun (t,_) -> fst (Term.destEvar (EConstr.Unsafe.to_constr t))) initial in
     { Evd.it = goals ; sigma=solution; }
 
   let top_evars initial =
     let evars_of_initial (c,_) =
-      Evar.Set.elements (Evd.evars_of_term c)
+      Evar.Set.elements (Evd.evars_of_term (EConstr.Unsafe.to_constr c))
     in
     CList.flatten (CList.map evars_of_initial initial)
 
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 2350592a2..9f10e874a 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -43,7 +43,7 @@ val compact : entry -> proofview -> entry * proofview
     empty [evar_map] (indeed a proof can be triggered by an incomplete
     pretyping), [init] takes an additional argument to represent the
     initial [evar_map]. *)
-val init : Evd.evar_map -> (Environ.env * Term.types) list -> entry * proofview
+val init : Evd.evar_map -> (Environ.env * EConstr.types) list -> entry * proofview
 
 (** A [telescope] is a list of environment and conclusion like in
     {!init}, except that each element may depend on the previous
@@ -52,7 +52,7 @@ val init : Evd.evar_map -> (Environ.env * Term.types) list -> entry * proofview
     [evar_map] is threaded in state passing style. *)
 type telescope =
   | TNil of Evd.evar_map
-  | TCons of Environ.env * Evd.evar_map * Term.types * (Evd.evar_map -> Term.constr -> telescope)
+  | TCons of Environ.env * Evd.evar_map * EConstr.types * (Evd.evar_map -> EConstr.constr -> telescope)
 
 (** Like {!init}, but goals are allowed to be dependent on one
     another. Dependencies between goals is represented with the type
@@ -69,8 +69,8 @@ val finished : proofview -> bool
 (** Returns the current [evar] state. *)
 val return : proofview -> Evd.evar_map
 
-val partial_proof : entry -> proofview -> constr list
-val initial_goals : entry -> (constr * types) list
+val partial_proof : entry -> proofview -> EConstr.constr list
+val initial_goals : entry -> (EConstr.constr * EConstr.types) list
 
 
 
diff --git a/engine/termops.mli b/engine/termops.mli
index 3f924cfa1..196962354 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -12,8 +12,8 @@
 open Pp
 open Names
 open Term
-open EConstr
 open Environ
+open EConstr
 
 (** printers *)
 val print_sort : sorts -> std_ppcmds
@@ -283,4 +283,4 @@ val on_judgment_type  : ('t -> 't) -> ('c, 't) punsafe_judgment -> ('c, 't) puns
 
 (** {6 Functions to deal with impossible cases } *)
 val set_impossible_default_clause : (unit -> (Constr.constr * Constr.types) Univ.in_universe_context_set) -> unit
-val coq_unit_judge : unit -> EConstr.unsafe_judgment Univ.in_universe_context_set
+val coq_unit_judge : unit -> unsafe_judgment Univ.in_universe_context_set