diff options
| author | herbelin | 2002-05-29 10:59:21 +0000 |
|---|---|---|
| committer | herbelin | 2002-05-29 10:59:21 +0000 |
| commit | 6a2eeb9e43b18c780168b80b2950da3e5850e942 (patch) | |
| tree | 5f0eae1ba0b5b0f9f1008822056e11d97e4552ac /tactics/Setoid_replace.v | |
| parent | 49485357eb8cd7f1820bd984f1833282f96cd656 (diff) | |
Fichiers tactics/*.ml4 remplacent les tactics/*.v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2724 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/Setoid_replace.v')
| -rw-r--r-- | tactics/Setoid_replace.v | 31 |
1 files changed, 0 insertions, 31 deletions
diff --git a/tactics/Setoid_replace.v b/tactics/Setoid_replace.v deleted file mode 100644 index 1261927580..0000000000 --- a/tactics/Setoid_replace.v +++ /dev/null @@ -1,31 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) - -(* $Id$: *) - -Grammar tactic simple_tactic : ast := - setoid_replace [ "Setoid_replace" constrarg($c1) "with" constrarg($c2) ] -> [(Setoid_replace $c1 $c2)] -. - -Grammar tactic simple_tactic : ast := - setoid_rewriteLR [ "Setoid_rewrite" "->" constrarg($c) ] -> [(Setoid_rewriteLR $c)] -| setoid_rewriteRL [ "Setoid_rewrite" "<-" constrarg($c) ] -> [(Setoid_rewriteRL $c)] -| setoid_rewrite [ "Setoid_rewrite" constrarg($c) ] -> [(Setoid_rewriteLR $c)] -. - -Syntax tactic level 0 : - setoid_replace [<<(Setoid_replace $c1 $c2)>>] -> [[<hov 0>"Setoid_replace " $c1 [1 1] "with " $c2]] - | setoid_rewritelr [<<(Setoid_rewriteLR $c)>>] -> ["Setoid_rewrite " $c] - | setoid_rewriterl [<<(Setoid_rewriteRL $c)>>] -> ["Setoid_rewrite <- " $c] -. - -Grammar vernac vernac : ast := - add_setoid [ "Add" "Setoid" constrarg($a) constrarg($aeq) constrarg($t) "." ] - -> [(AddSetoid $a $aeq $t)] -| new_morphism [ "Add" "Morphism" constrarg($m) ":" identarg($s) "." ] -> [(NamedNewMorphism $s $m)] -. |