diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proof.ml | 4 | ||||
| -rw-r--r-- | proofs/proof.mli | 2 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 2 | ||||
| -rw-r--r-- | proofs/proofview.ml | 4 | ||||
| -rw-r--r-- | proofs/proofview.mli | 2 |
5 files changed, 7 insertions, 7 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml index 1dca04336f..35166def01 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -226,9 +226,9 @@ let end_of_stack = CondEndStack end_of_stack_kind let unfocused = is_last_focus end_of_stack_kind -let start goals = +let start sigma goals = let pr = { - proofview = Proofview.init goals ; + proofview = Proofview.init sigma goals ; focus_stack = [] ; shelf = [] ; given_up = [] } in diff --git a/proofs/proof.mli b/proofs/proof.mli index 48333285d4..b9c3aa1b0a 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -53,7 +53,7 @@ val proof : proof -> (*** General proof functions ***) -val start : (Environ.env * Term.types) list -> proof +val start : Evd.evar_map -> (Environ.env * Term.types) list -> proof val initial_goals : proof -> (Term.constr * Term.types) list (* Returns [true] if the considered proof is completed, that is if no goal remain diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index ac61f4e679..12a5285043 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -239,7 +239,7 @@ end let start_proof id str goals ?(compute_guard=[]) hook = let initial_state = { pid = id; - proof = Proof.start goals; + proof = Proof.start Evd.empty goals; endline_tactic = None; section_vars = None; strength = str; diff --git a/proofs/proofview.ml b/proofs/proofview.ml index bc251d33de..7eb32f34a2 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -31,10 +31,10 @@ let proofview p = (* Initialises a proofview, the argument is a list of environement, conclusion types, and optional names, creating that many initial goals. *) -let init = +let init sigma = let rec aux = function | [] -> { initial = [] ; - solution = Evd.empty ; + solution = sigma ; comb = []; } | (env,typ)::l -> let { initial = ret ; solution = sol ; comb = comb } = diff --git a/proofs/proofview.mli b/proofs/proofview.mli index c07613f672..2945fb7141 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -36,7 +36,7 @@ val proofview : proofview -> Goal.goal list * Evd.evar_map (* Initialises a proofview, the argument is a list of environement, conclusion types, creating that many initial goals. *) -val init : (Environ.env * Term.types) list -> proofview +val init : Evd.evar_map -> (Environ.env * Term.types) list -> proofview (* Returns whether this proofview is finished or not. That is, if it has empty subgoals in the comb. There could still be unsolved |