diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-11-29 19:05:53 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-11-29 19:13:30 +0100 |
commit | e98d3c3793f26265a49f63a6e78d704f88341df9 (patch) | |
tree | c0328afc0034f3262dca2ca067531ee19bbb0ee0 /proofs/pfedit.ml | |
parent | 103ec7205d9038f1f3821f9287e3bb0907a1e3ec (diff) | |
parent | 8d6e58e16cc53a3198eb4c4afef0a2c39f6a5c56 (diff) |
Merge branch 'v8.5'
Diffstat (limited to 'proofs/pfedit.ml')
-rw-r--r-- | proofs/pfedit.ml | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 86bc44a62..9f2a00135 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -20,14 +20,15 @@ let get_current_proof_name = Proof_global.get_current_proof_name let get_all_proof_names = Proof_global.get_all_proof_names type lemma_possible_guards = Proof_global.lemma_possible_guards +type universe_binders = Proof_global.universe_binders let delete_proof = Proof_global.discard let delete_current_proof = Proof_global.discard_current let delete_all_proofs = Proof_global.discard_all -let start_proof (id : Id.t) str sigma hyps c ?init_tac terminator = +let start_proof (id : Id.t) ?pl str sigma hyps c ?init_tac terminator = let goals = [ (Global.env_of_context hyps , c) ] in - Proof_global.start_proof sigma id str goals terminator; + Proof_global.start_proof sigma id ?pl str goals terminator; let env = Global.env () in ignore (Proof_global.with_current_proof (fun _ p -> match init_tac with @@ -54,6 +55,9 @@ let set_used_variables l = let get_used_variables () = Proof_global.get_used_variables () +let get_universe_binders () = + Proof_global.get_universe_binders () + exception NoSuchGoal let _ = Errors.register_handler begin function | NoSuchGoal -> Errors.error "No such goal." @@ -140,7 +144,7 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo let status = by tac in let _,(const,univs,_) = cook_proof () in delete_current_proof (); - const, status, univs + const, status, fst univs with reraise -> let reraise = Errors.push reraise in delete_current_proof (); |