aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
diff options
context:
space:
mode:
authorGravatar sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-10-01 16:33:00 +0000
committerGravatar sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-10-01 16:33:00 +0000
commit4eafa8d4cc44da82f528cf61508330a6a28355b2 (patch)
tree29372c79b77898304fcbceca55c637e5c34fc070 /tactics
parent0d34c71a1a02c5e2d1718b039a8da484a22cc068 (diff)
The "Add Setoid" command now has a new argument "as name" that is used
to generate the name of the morphism. Previously the name was automatically generated, but this behaviour was not compatible with module typing: it was not possible to generate the same identifier in the module type and in the module. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6168 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
-rw-r--r--tactics/extratactics.ml45
1 files changed, 3 insertions, 2 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index ff12e366c..f182570a5 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -195,11 +195,12 @@ TACTIC EXTEND SetoidRewrite
END
VERNAC COMMAND EXTEND AddSetoid1
- [ "Add" "Setoid" constr(a) constr(aeq) constr(t) ] -> [ add_setoid a aeq t ]
+ [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
+ [ add_setoid n a aeq t ]
| [ "Add" "Morphism" constr(m) ":" ident(n) ] ->
[ new_named_morphism n m None ]
| [ "Add" "Morphism" constr(m) "with" "signature" morphism_signature(s) "as" ident(n) ] ->
- [ new_named_morphism n m (Some s)]
+ [ new_named_morphism n m (Some s)]
END
VERNAC COMMAND EXTEND AddRelation1