From 26ad2343cccb08f5352dcd45043a58f49d11fa7f Mon Sep 17 00:00:00 2001
From: sacerdot
Date: Fri, 10 Sep 2004 14:09:53 +0000
Subject: Add_new_morphism has now a new optional argument that is the
 signature of the morphism.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6092 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/extratactics.ml4 | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 694e88801c..0d4b479b44 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -175,7 +175,8 @@ END
 
 VERNAC COMMAND EXTEND AddSetoid
   [ "Add" "Setoid" constr(a) constr(aeq) constr(t) ] -> [ add_setoid a aeq t ]
-| [ "Add" "Morphism" constr(m) ":" ident(s) ] -> [ new_named_morphism s m ]
+| [ "Add" "Morphism" constr(m) ":" ident(s) ] ->
+   [ new_named_morphism s m None ]
 END
 
 VERNAC COMMAND EXTEND AddRelation1
-- 
cgit v1.2.3