1 files changed, 12 insertions, 7 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index f45eb2a3a..3fc01c0bc 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -118,26 +118,28 @@ open Decl_kinds
 
 let next = let n = ref 0 in fun () -> incr n; !n
 
-let build_constant_by_tactic id sign ?(goal_kind = Global,Proof Theorem) typ tac =
+let build_constant_by_tactic id sign ?(goal_kind = Global, false, Proof Theorem) typ tac =
+  let substref = ref Univ.LMap.empty in (** FIXME: Something wrong here with subst *)
   start_proof id goal_kind sign typ (fun _ -> ());
   try
     let status = by tac in
     let _,(const,_) = cook_proof () in
     delete_current_proof ();
-    const, status
+    const, status, !substref
   with reraise ->
     let reraise = Errors.push reraise in
     delete_current_proof ();
     raise reraise
 
-let build_by_tactic env typ tac =
+let build_by_tactic env ?(poly=false) typ tac =
   let id = Id.of_string ("temporary_proof"^string_of_int (next())) in
   let sign = val_of_named_context (named_context env) in
-  let ce,status = build_constant_by_tactic id sign typ tac in
+  let gk = Global, poly, Proof Theorem in
+  let ce, status, subst = build_constant_by_tactic id sign ~goal_kind:gk typ tac in
   let ce = Term_typing.handle_side_effects env ce in
   let cb, se = Future.force ce.const_entry_body in
-  assert(Declareops.side_effects_is_empty (Declareops.no_seff));
-  cb,status
+  assert(Declareops.side_effects_is_empty se);
+  cb, status, subst
 
 (**********************************************************************)
 (* Support for resolution of evars in tactic interpretation, including
@@ -156,6 +158,9 @@ let solve_by_implicit_tactic env sigma evk =
       when
 	Context.named_context_equal (Environ.named_context_of_val evi.evar_hyps)
 	(Environ.named_context env) ->
-      (try fst (build_by_tactic env evi.evar_concl (Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (Errors.UserError ("",Pp.str"Proof is not complete."))) [])))
+      let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (Errors.UserError ("",Pp.str"Proof is not complete."))) []) in
+      (try
+        let (ans, _, _) = build_by_tactic env (evi.evar_concl, Evd.get_universe_context_set sigma) tac in
+        ans
        with e when Logic.catchable_exception e -> raise Exit)
   | _ -> raise Exit