diff options
Diffstat (limited to 'proofs/pfedit.ml')
| -rw-r--r-- | proofs/pfedit.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index b635cc963..20d696fd9 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -138,7 +138,8 @@ let next = let n = ref 0 in fun () -> incr n; !n let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theorem) typ tac = let evd = Evd.from_ctx ctx in - start_proof id goal_kind evd sign typ (fun _ -> ()); + let terminator = Proof_global.make_terminator (fun _ -> ()) in + start_proof id goal_kind evd sign typ terminator; try let status = by tac in let _,(const,univs,_) = cook_proof () in @@ -214,7 +215,7 @@ let solve_by_implicit_tactic env sigma evk = match (!implicit_tactic, snd (evar_source evk sigma)) with | Some tac, (Evar_kinds.ImplicitArg _ | Evar_kinds.QuestionMark _) when - Context.named_context_equal (Environ.named_context_of_val evi.evar_hyps) + Context.Named.equal (Environ.named_context_of_val evi.evar_hyps) (Environ.named_context env) -> let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (Errors.UserError ("",Pp.str"Proof is not complete."))) []) in (try |