diff options
| author | herbelin | 2007-04-28 09:34:32 +0000 |
|---|---|---|
| committer | herbelin | 2007-04-28 09:34:32 +0000 |
| commit | b61d0df2899f5de9c20ee4a2c4b79deb0714b162 (patch) | |
| tree | 6c548a7046878591025baae80b4ead8d5b349c2a /proofs | |
| parent | 2ed87ba29db49e043062e125f3783a553d550fc4 (diff) | |
Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.
Fusion des syntaxes de "apply" et "eapply". Ajout de "eapply in",
"erewrite" et "erewrite in". Correction au passage des bugs #1461 et
#1522).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9802 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/tacexpr.ml | 5 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 2 |
2 files changed, 4 insertions, 3 deletions
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index 633a9a42d3..14794086ab 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -21,6 +21,7 @@ type 'a or_metaid = AI of 'a | MetaId of loc * string type direction_flag = bool (* true = Left-to-right false = right-to-right *) type lazy_flag = bool (* true = lazy false = eager *) +type evars_flag = bool (* true = pose evars false = fail on evars *) type raw_red_flag = | FBeta @@ -122,7 +123,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = | TacExact of 'constr | TacExactNoCheck of 'constr | TacVmCastNoCheck of 'constr - | TacApply of 'constr with_bindings + | TacApply of evars_flag * 'constr with_bindings | TacElim of 'constr with_bindings * 'constr with_bindings option | TacElimType of 'constr | TacCase of 'constr with_bindings @@ -184,7 +185,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = | TacTransitivity of 'constr (* Equality and inversion *) - | TacRewrite of bool * 'constr with_bindings * 'id gclause + | TacRewrite of bool * evars_flag * 'constr with_bindings * 'id gclause | TacInversion of ('constr,'id) inversion_strength * quantified_hypothesis (* For ML extensions *) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 06178324d9..2049eb0f6a 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -235,7 +235,7 @@ let thin l = with_check (thin_no_check l) let thin_body c = with_check (thin_body_no_check c) let move_hyp b id id' = with_check (move_hyp_no_check b id id') let rename_hyp id id' = with_check (rename_hyp_no_check id id') - + (* Pretty-printers *) open Pp |