diff options
| author | clrenard | 2001-09-18 13:09:47 +0000 |
|---|---|---|
| committer | clrenard | 2001-09-18 13:09:47 +0000 |
| commit | b915d23eefe20c6ca9d744807c9c18b91d9fc1df (patch) | |
| tree | 5586f10324661711386ebaccda28dccb0f1e9514 /tactics | |
| parent | 1f78733204d5a1232d06c103057dc65dcb14a7ea (diff) | |
Modification de l'emplacement des fichiers pour les setoides.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1982 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/Setoid_replace.v | 31 | ||||
| -rw-r--r-- | tactics/setoid_replace.ml | 12 |
2 files changed, 37 insertions, 6 deletions
diff --git a/tactics/Setoid_replace.v b/tactics/Setoid_replace.v new file mode 100644 index 0000000000..1261927580 --- /dev/null +++ b/tactics/Setoid_replace.v @@ -0,0 +1,31 @@ +(***********************************************************************) +(* 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)] +. diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 613c0a475c..f7eb0bbd42 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -39,7 +39,7 @@ type morphism = let constr_of c = Astterm.interp_constr Evd.empty (Global.env()) c let constant dir s = - let dir = make_dirpath (List.map id_of_string ("Coq"::"Setoid"::dir)) in + let dir = make_dirpath (List.map id_of_string ("Coq"::"Init"::dir)) in let id = id_of_string s in try Declare.global_reference_in_absolute_module dir id @@ -62,13 +62,13 @@ let current_constant id = (* Setoid_theory *) -let coq_Setoid_Theory = lazy(constant ["Setoid_replace"] "Setoid_Theory") +let coq_Setoid_Theory = lazy(constant ["Setoid"] "Setoid_Theory") -let coq_seq_refl = lazy(constant ["Setoid_replace"] "Seq_refl") -let coq_seq_sym = lazy(constant ["Setoid_replace"] "Seq_sym") -let coq_seq_trans = lazy(constant ["Setoid_replace"] "Seq_trans") +let coq_seq_refl = lazy(constant ["Setoid"] "Seq_refl") +let coq_seq_sym = lazy(constant ["Setoid"] "Seq_sym") +let coq_seq_trans = lazy(constant ["Setoid"] "Seq_trans") -let coq_fleche = lazy(constant ["Setoid_replace"] "fleche") +let coq_fleche = lazy(constant ["Setoid"] "fleche") (* Coq constants *) |