diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenvtac.ml | 1 | ||||
| -rw-r--r-- | proofs/proof_type.ml | 6 | ||||
| -rw-r--r-- | proofs/proof_type.mli | 6 | ||||
| -rw-r--r-- | proofs/refiner.mli | 5 |
4 files changed, 12 insertions, 6 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index ff7cf5acc3..9bc818e861 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -78,6 +78,7 @@ let clenv_refine with_evars ?(with_classes=true) clenv gls = clenv.env clenv.evd else clenv.evd in + let clenv = { clenv with evd = evd' } in tclTHEN (tclEVARS evd') (refine (clenv_cast_meta clenv (clenv_value clenv))) diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index e7bca648c8..bc29534081 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -63,7 +63,7 @@ and tactic = goal sigma -> (goal list sigma * validation) and validation = (proof_tree list -> proof_tree) and tactic_expr = - (open_constr, + (constr, constr_pattern, evaluable_global_reference, inductive, @@ -74,7 +74,7 @@ and tactic_expr = Tacexpr.gen_tactic_expr and atomic_tactic_expr = - (open_constr, + (constr, constr_pattern, evaluable_global_reference, inductive, @@ -85,7 +85,7 @@ and atomic_tactic_expr = Tacexpr.gen_atomic_tactic_expr and tactic_arg = - (open_constr, + (constr, constr_pattern, evaluable_global_reference, inductive, diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index 5fa4a44ef7..b5c4a234d1 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -98,7 +98,7 @@ and tactic = goal sigma -> (goal list sigma * validation) and validation = (proof_tree list -> proof_tree) and tactic_expr = - (open_constr, + (constr, constr_pattern, evaluable_global_reference, inductive, @@ -109,7 +109,7 @@ and tactic_expr = Tacexpr.gen_tactic_expr and atomic_tactic_expr = - (open_constr, + (constr, constr_pattern, evaluable_global_reference, inductive, @@ -120,7 +120,7 @@ and atomic_tactic_expr = Tacexpr.gen_atomic_tactic_expr and tactic_arg = - (open_constr, + (constr, constr_pattern, evaluable_global_reference, inductive, diff --git a/proofs/refiner.mli b/proofs/refiner.mli index ff902d880b..e853c12b7c 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -185,6 +185,11 @@ val then_tactic_list : tactic_list -> tactic_list -> tactic_list val tactic_list_tactic : tactic_list -> tactic val goal_goal_list : 'a sigma -> 'a list sigma +(* [tclWITHHOLES solve_holes tac (sigma,c)] applies [tac] to [c] which + may have unresolved holes; if [solve_holes] these holes must be + resolved after application of the tactic; [sigma] must be an + extension of the sigma of the goal *) +val tclWITHHOLES : bool -> ('a -> tactic) -> evar_map -> 'a -> tactic (*s Functions for handling the state of the proof editor. *) |