Evar-normalizing functions now act on EConstrs.

6 files changed, 18 insertions, 15 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index af910810b..142fd9a89 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -199,6 +199,7 @@ let refine_by_tactic env sigma ty tac =
   | _ -> assert false
   in
   let ans = Reductionops.nf_evar sigma ans in
+  let ans = EConstr.Unsafe.to_constr ans in
   (** [neff] contains the freshly generated side-effects *)
   let neff = Evd.eval_side_effects sigma in
   (** Reset the old side-effects *)
@@ -232,7 +233,8 @@ let solve_by_implicit_tactic env sigma evk =
       let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (CErrors.UserError (None,Pp.str"Proof is not complete."))) []) in
       (try
         let c = Evarutil.nf_evars_universes sigma evi.evar_concl in
-        if Evarutil.has_undefined_evars sigma (EConstr.of_constr c) then raise Exit;
+        let c = EConstr.of_constr c in
+        if Evarutil.has_undefined_evars sigma c then raise Exit;
         let (ans, _, ctx) =
 	  build_by_tactic env (Evd.evar_universe_context sigma) c tac in
         let sigma = Evd.set_universe_context sigma ctx in
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 807a554df..516125ea1 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -60,7 +60,7 @@ type lemma_possible_guards = Proof_global.lemma_possible_guards
 type universe_binders = Id.t Loc.located list
 
 val start_proof :
-  Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map -> named_context_val -> constr ->
+  Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map -> named_context_val -> EConstr.constr ->
   ?init_tac:unit Proofview.tactic ->
   Proof_global.proof_terminator -> unit
 
@@ -106,7 +106,7 @@ val get_current_context : unit -> Evd.evar_map * env
 (** [current_proof_statement] *)
 
 val current_proof_statement :
-  unit -> Id.t * goal_kind * types
+  unit -> Id.t * goal_kind * EConstr.types
 
 (** {6 ... } *)
 (** [get_current_proof_name ()] return the name of the current focused
@@ -166,15 +166,15 @@ val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> unit
 
 val build_constant_by_tactic :
   Id.t -> Evd.evar_universe_context -> named_context_val -> ?goal_kind:goal_kind ->
-  types -> unit Proofview.tactic -> 
+  EConstr.types -> unit Proofview.tactic -> 
   Safe_typing.private_constants Entries.definition_entry * bool *
     Evd.evar_universe_context
 
 val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?poly:polymorphic ->
-  types -> unit Proofview.tactic -> 
+  EConstr.types -> unit Proofview.tactic -> 
   constr * bool * Evd.evar_universe_context
 
-val refine_by_tactic : env -> Evd.evar_map -> types -> unit Proofview.tactic ->
+val refine_by_tactic : env -> Evd.evar_map -> EConstr.types -> unit Proofview.tactic ->
   constr * Evd.evar_map
 (** A variant of the above function that handles open terms as well.
     Caveat: all effects are purged in the returned term at the end, but other
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 5053fc7fb..8dcc5b76e 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -66,9 +66,9 @@ val map_structured_proof : proof -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre
 
 (*** General proof functions ***)
 
-val start : Evd.evar_map -> (Environ.env * Term.types) list -> proof
+val start : Evd.evar_map -> (Environ.env * EConstr.types) list -> proof
 val dependent_start : Proofview.telescope -> proof
-val initial_goals : proof -> (Term.constr * Term.types) list
+val initial_goals : proof -> (EConstr.constr * EConstr.types) list
 val initial_euctx : proof -> Evd.evar_universe_context
 
 (* Returns [true] if the considered proof is completed, that is if no goal remain
@@ -79,7 +79,7 @@ val is_done : proof -> bool
 val is_complete : proof -> bool
 
 (* Returns the list of partial proofs to initial goals. *)
-val partial_proof : proof -> Term.constr list
+val partial_proof : proof -> EConstr.constr list
 
 val compact : proof -> proof
 
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 2956d623f..eb1bea897 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -375,6 +375,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
   in
   let entries =
     Future.map2 (fun p (_, t) ->
+      let t = EConstr.Unsafe.to_constr t in
       let univstyp, body = make_body t p in
       let univs, typ = Future.force univstyp in
 	{ Entries.
@@ -406,7 +407,7 @@ let return_proof ?(allow_partial=false) () =
   (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
       side-effects... This may explain why one need to uniquize side-effects
       thereafter... *)
-  let proofs = List.map (fun c -> c, eff) proofs in
+  let proofs = List.map (fun c -> EConstr.Unsafe.to_constr c, eff) proofs in
     proofs, Evd.evar_universe_context evd
  end else
   let initial_goals = Proof.initial_goals proof in
@@ -430,7 +431,7 @@ let return_proof ?(allow_partial=false) () =
       side-effects... This may explain why one need to uniquize side-effects
       thereafter... *)
   let proofs = 
-    List.map (fun (c, _) -> (Evarutil.nf_evars_universes evd c, eff)) initial_goals in
+    List.map (fun (c, _) -> (Evarutil.nf_evars_universes evd (EConstr.Unsafe.to_constr c), eff)) initial_goals in
     proofs, Evd.evar_universe_context evd
 
 let close_future_proof ~feedback_id proof =
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 97a21cf22..3b2cc6b23 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -86,7 +86,7 @@ val apply_terminator : proof_terminator -> proof_ending -> unit
     end of the proof to close the proof. *)
 val start_proof :
   Evd.evar_map -> Names.Id.t -> ?pl:universe_binders ->
-  Decl_kinds.goal_kind -> (Environ.env * Term.types) list  ->
+  Decl_kinds.goal_kind -> (Environ.env * EConstr.types) list  ->
     proof_terminator -> unit
 
 (** Like [start_proof] except that there may be dependencies between
@@ -201,7 +201,7 @@ end
 val get_default_goal_selector : unit -> Vernacexpr.goal_selector
 
 module V82 : sig
-  val get_current_initial_conclusions : unit -> Names.Id.t *(Term.types list *
+  val get_current_initial_conclusions : unit -> Names.Id.t *(EConstr.types list *
   Decl_kinds.goal_kind)
 end
 
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 2fab026ea..3ed262d6e 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -223,7 +223,7 @@ module New = struct
     let gl = Proofview.Goal.assume gl in
     let concl = Proofview.Goal.concl gl in
     let sigma = project gl in
-    EConstr.of_constr (nf_evar sigma (EConstr.Unsafe.to_constr concl))
+    nf_evar sigma concl
 
   let pf_whd_all gl t = pf_apply whd_all gl t
 
@@ -241,6 +241,6 @@ module New = struct
   let pf_whd_all gl t = pf_apply whd_all gl t
   let pf_compute gl t = pf_apply compute gl t
 
-  let pf_nf_evar gl t = EConstr.of_constr (nf_evar (project gl) (EConstr.Unsafe.to_constr t))
+  let pf_nf_evar gl t = nf_evar (project gl) t
 
 end