Evar-normalizing functions now act on EConstrs.

3 files changed, 9 insertions, 7 deletions

diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index e3f1c1ac28..77fb960e16 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -449,7 +449,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
         List.iter (fun (strength,ref,imps) ->
 	  maybe_declare_manual_implicits false ref imps;
 	  call_hook (fun exn -> exn) hook strength ref) thms_data in
-      start_proof_univs id ?pl kind ctx t ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard
+      start_proof_univs id ?pl kind ctx (EConstr.of_constr t) ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard
 
 let start_proof_com ?inference_hook kind thms hook =
   let env0 = Global.env () in
@@ -461,13 +461,12 @@ let start_proof_com ?inference_hook kind thms hook =
   let thms = List.map (fun (sopt,(bl,t,guard)) ->
     let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in
     let t', imps' = interp_type_evars_impls ~impls env evdref t in
-    let t' = EConstr.Unsafe.to_constr t' in
     let flags = all_and_fail_flags in
     let flags = { flags with use_hook = inference_hook } in
     evdref := solve_remaining_evars flags env !evdref (Evd.empty,!evdref);
     let ids = List.map RelDecl.get_name ctx in
       (compute_proof_name (pi1 kind) sopt,
-      (nf_evar !evdref (Term.it_mkProd_or_LetIn t' ctx),
+      (EConstr.Unsafe.to_constr (nf_evar !evdref (EConstr.it_mkProd_or_LetIn t' ctx)),
        (ids, imps @ lift_implicits (List.length ids) imps'),
        guard)))
     thms in
@@ -519,6 +518,7 @@ let save_proof ?proof = function
         | None ->
             let pftree = Pfedit.get_pftreestate () in
             let id, k, typ = Pfedit.current_proof_statement () in
+            let typ = EConstr.Unsafe.to_constr typ in
             let universes = Proof.initial_euctx pftree in
             (* This will warn if the proof is complete *)
             let pproofs, _univs =
diff --git a/stm/lemmas.mli b/stm/lemmas.mli
index 39c089be9f..681413a297 100644
--- a/stm/lemmas.mli
+++ b/stm/lemmas.mli
@@ -19,17 +19,17 @@ val call_hook :
   Future.fix_exn -> 'a declaration_hook -> Decl_kinds.locality -> Globnames.global_reference -> 'a
 
 (** A hook start_proof calls on the type of the definition being started *)
-val set_start_hook : (types -> unit) -> unit
+val set_start_hook : (EConstr.types -> unit) -> unit
 
 val start_proof : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map ->
   ?terminator:(lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) ->
-  ?sign:Environ.named_context_val -> types ->
+  ?sign:Environ.named_context_val -> EConstr.types ->
   ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> 
    unit declaration_hook -> unit
 
 val start_proof_univs : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map ->
   ?terminator:(lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> Proof_global.proof_terminator) ->
-  ?sign:Environ.named_context_val -> types ->
+  ?sign:Environ.named_context_val -> EConstr.types ->
   ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> 
   (Evd.evar_universe_context option -> unit declaration_hook) -> unit
 
diff --git a/stm/stm.ml b/stm/stm.ml
index d60412c0cd..47e806929b 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1719,8 +1719,10 @@ end = struct (* {{{ *)
         match Evd.(evar_body (find sigma r_goal)) with
         | Evd.Evar_empty -> RespNoProgress
         | Evd.Evar_defined t ->
+            let t = EConstr.of_constr t in
             let t = Evarutil.nf_evar sigma t in
-            if Evarutil.is_ground_term sigma (EConstr.of_constr t) then
+            if Evarutil.is_ground_term sigma t then
+              let t = EConstr.Unsafe.to_constr t in
               RespBuiltSubProof (t, Evd.evar_universe_context sigma)
             else CErrors.user_err ~hdr:"STM" (str"The solution is not ground")
        end) ()