Change the interface of proof_global to take an evar_map instead of a universe context to start proofs.

It was kind of awkward to work with for non-traditionnal kinds of proofs: if you have an evar_universe_context, you got it from a sigma anyway.

3 files changed, 12 insertions, 10 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index d3410ea751..0c4250535b 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -27,7 +27,7 @@ let delete_all_proofs = Proof_global.discard_all
 
 let start_proof (id : Id.t) str ctx hyps c ?init_tac terminator =
   let goals = [ (Global.env_of_context hyps , c) ] in
-  Proof_global.start_proof id str ctx goals terminator;
+  Proof_global.start_proof (Evd.from_env ~ctx (Global.env ())) id str goals terminator;
   let env = Global.env () in
   ignore (Proof_global.with_current_proof (fun _ p ->
     match init_tac with
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 7c7ff0c940..8a3c0f775a 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -216,28 +216,30 @@ let activate_proof_mode mode =
 let disactivate_proof_mode mode =
   Ephemeron.iter_opt (find_proof_mode mode) (fun x -> x.reset ())
 
-(** [start_proof id str goals terminator] starts a proof of name [id]
-    with goals [goals] (a list of pairs of environment and
+(** [start_proof sigma id str goals terminator] starts a proof of name
+    [id] with goals [goals] (a list of pairs of environment and
     conclusion); [str] describes what kind of theorem/definition this
     is (spiwack: for potential printing, I believe is used only by
     closing commands and the xml plugin); [terminator] is used at the
-    end of the proof to close the proof. *)
-let start_proof id str ctx goals terminator =
+    end of the proof to close the proof. The proof is started in the
+    evar map [sigma] (which can typically contain universe
+    constraints). *)
+let start_proof sigma id str goals terminator =
   let initial_state = {
     pid = id;
     terminator = Ephemeron.create terminator;
-    proof = Proof.start (Evd.from_env ~ctx (Global.env ())) goals;
+    proof = Proof.start sigma goals;
     endline_tactic = None;
     section_vars = None;
     strength = str;
     mode = find_proof_mode "No" } in
   push initial_state pstates
 
-let start_dependent_proof id str ctx goals terminator =
+let start_dependent_proof sigma id str goals terminator =
   let initial_state = {
     pid = id;
     terminator = Ephemeron.create terminator;
-    proof = Proof.dependent_start (Evd.from_env ~ctx (Global.env ())) goals;
+    proof = Proof.dependent_start sigma goals;
     endline_tactic = None;
     section_vars = None;
     strength = str;
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 2b54b24ef2..be01229c9f 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -78,13 +78,13 @@ type closed_proof = proof_object * proof_terminator
     closing commands and the xml plugin); [terminator] is used at the
     end of the proof to close the proof. *)
 val start_proof :
-  Names.Id.t -> Decl_kinds.goal_kind -> Evd.evar_universe_context -> (Environ.env * Term.types) list  ->
+  Evd.evar_map -> Names.Id.t -> Decl_kinds.goal_kind -> (Environ.env * Term.types) list  ->
     proof_terminator -> unit
 
 (** Like [start_proof] except that there may be dependencies between
     initial goals. *)
 val start_dependent_proof :
-  Names.Id.t -> Decl_kinds.goal_kind -> Evd.evar_universe_context -> Proofview.telescope  ->
+  Evd.evar_map -> Names.Id.t -> Decl_kinds.goal_kind -> Proofview.telescope  ->
     proof_terminator -> unit
 
 (* Takes a function to add to the exceptions data relative to the