diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/lemmas.ml | 10 | ||||
| -rw-r--r-- | stm/lemmas.mli | 6 |
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 |