diff options
| author |  bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-01-28 08:32:21 +0000 |
|---|---|---|
| committer | bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-01-28 08:32:21 +0000 |
| commit | 1091a134df7d3af4cacde58b09c230619f7739a0 (patch) | |
| tree | 902b58f6c675a4ad541348f96df0267448b80a9e /contrib/interface/vtp.ml | |
| parent | 81c7b237f71d571098371018fc903552768dab2a (diff) | |
make sure that 'in' clauses for reduction tactics are translated
once again re-organize the way intro patterns are translated: there is now
only one kind of pattern that can be used for both and and or constructs:
the use of the multiplet notation should only be a matter of notation.
un-capitalize a few tactic names for tactics represented using the TacExtend
construct.
corrects a bug in the way binders or coercion binders were used.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5260 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/interface/vtp.ml')
| -rw-r--r-- | contrib/interface/vtp.ml | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml index 3a2c9b1cb..037e48fe2 100644 --- a/contrib/interface/vtp.ml +++ b/contrib/interface/vtp.ml @@ -917,10 +917,6 @@ and fINT = function (f_atom_int x); print_string "\n"and fINTRO_PATT = function | CT_coerce_ID_to_INTRO_PATT x -> fID x -| CT_conj_pattern(x,l) -> - fINTRO_PATT_LIST x; - (List.iter fINTRO_PATT_LIST l); - fNODE "conj_pattern" (1 + (List.length l)) | CT_disj_pattern(x,l) -> fINTRO_PATT_LIST x; (List.iter fINTRO_PATT_LIST l); |