Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.

As simple as this looks, there's been some quite subtle issues in doing this modification, there may be bugs left.

2 files changed, 8 insertions, 8 deletions

diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 0bcefc0e6a..560e662a19 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -350,7 +350,7 @@ let universe_proof_terminator compute_guard hook =
           save_anonymous_with_strength proof kind id
       end
 
-let start_proof id kind ctx ?sign c ?init_tac ?(compute_guard=[]) hook =
+let start_proof id kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook =
   let terminator = standard_proof_terminator compute_guard hook in
   let sign = 
     match sign with
@@ -358,9 +358,9 @@ let start_proof id kind ctx ?sign c ?init_tac ?(compute_guard=[]) hook =
     | None -> initialize_named_context_for_proof ()
   in
   !start_hook c;
-  Pfedit.start_proof id kind ctx sign c ?init_tac terminator
+  Pfedit.start_proof id kind sigma sign c ?init_tac terminator
 
-let start_proof_univs id kind ctx ?sign c ?init_tac ?(compute_guard=[]) hook =
+let start_proof_univs id kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook =
   let terminator = universe_proof_terminator compute_guard hook in
   let sign = 
     match sign with
@@ -368,7 +368,7 @@ let start_proof_univs id kind ctx ?sign c ?init_tac ?(compute_guard=[]) hook =
     | None -> initialize_named_context_for_proof ()
   in
   !start_hook c;
-  Pfedit.start_proof id kind ctx sign c ?init_tac terminator
+  Pfedit.start_proof id kind sigma sign c ?init_tac terminator
 
 let rec_tac_initializer finite guard thms snl =
   if finite then
@@ -446,7 +446,7 @@ let start_proof_com kind thms hook =
   let recguard,thms,snl = look_for_possibly_mutual_statements thms in
   let evd, nf = Evarutil.nf_evars_and_universes !evdref in
   let thms = List.map (fun (n, (t, info)) -> (n, (nf t, info))) thms in
-  start_proof_with_initialization kind (Evd.evar_universe_context evd) 
+  start_proof_with_initialization kind evd
     recguard thms snl hook
 
 
diff --git a/stm/lemmas.mli b/stm/lemmas.mli
index b77413bc9f..1d08b8fcef 100644
--- a/stm/lemmas.mli
+++ b/stm/lemmas.mli
@@ -25,11 +25,11 @@ val call_hook :
 (** A hook start_proof calls on the type of the definition being started *)
 val set_start_hook : (types -> unit) -> unit
 
-val start_proof : Id.t -> goal_kind -> Evd.evar_universe_context -> ?sign:Environ.named_context_val -> types ->
+val start_proof : Id.t -> goal_kind -> Evd.evar_map -> ?sign:Environ.named_context_val -> types ->
   ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> 
    unit declaration_hook -> unit
 
-val start_proof_univs : Id.t -> goal_kind -> Evd.evar_universe_context -> ?sign:Environ.named_context_val -> types ->
+val start_proof_univs : Id.t -> goal_kind -> Evd.evar_map -> ?sign:Environ.named_context_val -> types ->
   ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> 
   (Proof_global.proof_universes option -> unit declaration_hook) -> unit
 
@@ -38,7 +38,7 @@ val start_proof_com : goal_kind ->
   unit declaration_hook -> unit
 
 val start_proof_with_initialization : 
-  goal_kind -> Evd.evar_universe_context -> (bool * lemma_possible_guards * unit Proofview.tactic list option) option ->
+  goal_kind -> Evd.evar_map -> (bool * lemma_possible_guards * unit Proofview.tactic list option) option ->
   (Id.t * (types * (Name.t list * Impargs.manual_explicitation list))) list
   -> int list option -> unit declaration_hook -> unit