From 4eafa8d4cc44da82f528cf61508330a6a28355b2 Mon Sep 17 00:00:00 2001
From: sacerdot
Date: Fri, 1 Oct 2004 16:33:00 +0000
Subject: 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
---
 tactics/extratactics.ml4 | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index ff12e366cf..f182570a5f 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
-- 
cgit v1.2.3