Hugly temporary notation

 Add Morphism constr @ arugments_list @ output as name

replaced with the nicer (stable?) notation

 Add Morphism constr with signature signature as name


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6149 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 30 insertions, 24 deletions

diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index 119f6b3bf1..3ac4c5d7dc 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -34,14 +34,18 @@ ARGUMENT EXTEND orient TYPED AS bool PRINTED BY pr_orient
 END
 
 (* For Setoid rewrite *)
-let pr_morphism_argument _ _ = Setoid_replace.pr_morphism_argument
-
-ARGUMENT EXTEND morphism_argument
- TYPED AS morphism_argument
- PRINTED BY pr_morphism_argument
-  | [ constr(c) "++>" ] -> [ Some true,c ]
-  | [ constr(c) "-->" ] -> [ Some false,c ]
-  | [ constr(c) "==>"  ] -> [ None,c ]
+let pr_morphism_signature _ _ = Setoid_replace.pr_morphism_signature
+
+ARGUMENT EXTEND morphism_signature
+ TYPED AS morphism_signature
+ PRINTED BY pr_morphism_signature
+  | [ constr(out) ] -> [ [],out ]
+  | [ constr(c) "++>" morphism_signature(s) ] ->
+       [ let l,out = s in (Some true,c)::l,out ]
+  | [ constr(c) "-->" morphism_signature(s) ] ->
+       [ let l,out = s in (Some false,c)::l,out ]
+  | [ constr(c) "==>" morphism_signature(s) ] ->
+       [ let l,out = s in (None,c)::l,out ]
 END
 
 let pr_gen prc _ c = prc c
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index 81a3851522..ec3a990acc 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -19,12 +19,12 @@ val rawwit_orient : bool raw_abstract_argument_type
 val wit_orient : bool closed_abstract_argument_type
 val orient : bool Pcoq.Gram.Entry.e
 
-val rawwit_morphism_argument :
- Setoid_replace.morphism_argument raw_abstract_argument_type
-val wit_morphism_argument :
- Setoid_replace.morphism_argument closed_abstract_argument_type
-val morphism_argument :
- Setoid_replace.morphism_argument Pcoq.Gram.Entry.e
+val rawwit_morphism_signature :
+ Setoid_replace.morphism_signature raw_abstract_argument_type
+val wit_morphism_signature :
+ Setoid_replace.morphism_signature closed_abstract_argument_type
+val morphism_signature :
+ Setoid_replace.morphism_signature Pcoq.Gram.Entry.e
 
 val rawwit_raw : constr_expr raw_abstract_argument_type
 val wit_raw : rawconstr closed_abstract_argument_type
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 789e5c116c..8b5b224659 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -175,10 +175,10 @@ END
 
 VERNAC COMMAND EXTEND AddSetoid1
   [ "Add" "Setoid" constr(a) constr(aeq) constr(t) ] -> [ add_setoid a aeq t ]
-| [ "Add" "Morphism" constr(m) ":" ident(s) ] ->
-   [ new_named_morphism s m None ]
-| [ "Add" "Morphism" constr(m) "@" ne_morphism_argument_list(l) "@" constr(out) "as" ident(s) ] ->
-    [ new_named_morphism s m (Some (l,out))]
+| [ "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)]
 END
 
 VERNAC COMMAND EXTEND AddRelation1
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index ef09d9489f..6360799797 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -219,7 +219,9 @@ let prmorphism_argument_gen prrelation (variance,rel) =
 
 let prargument_class = prmorphism_argument_gen prrelation_class
 
-let pr_morphism_argument = prmorphism_argument_gen Ppconstrnew.pr_constr
+let pr_morphism_signature (l,c) =
+ prlist (prmorphism_argument_gen Ppconstrnew.pr_constr) l ++
+  Ppconstrnew.pr_constr c
 
 let prmorphism k m =
   prterm k ++ str ": " ++
@@ -698,7 +700,8 @@ let morphism_hook stre ref =
     add_morphism (Some (pf_id,argsconstr,outputconstr)) mor_id
      (m,args,output); no_more_edited pf_id
 
-type morphism_argument = bool option * Topconstr.constr_expr
+type morphism_signature =
+ (bool option * Topconstr.constr_expr) list * Topconstr.constr_expr
 
 let new_named_morphism id m sign =
  let sign =
diff --git a/tactics/setoid_replace.mli b/tactics/setoid_replace.mli
index babd89f1a8..eb2112a3b5 100644
--- a/tactics/setoid_replace.mli
+++ b/tactics/setoid_replace.mli
@@ -13,9 +13,9 @@ open Proof_type
 open Topconstr
 
 
-type morphism_argument = bool option * constr_expr
+type morphism_signature = (bool option * constr_expr) list * constr_expr
 
-val pr_morphism_argument : morphism_argument -> Pp.std_ppcmds
+val pr_morphism_signature : morphism_signature -> Pp.std_ppcmds
 
 val register_replace : (constr -> constr -> tactic) -> unit
 
@@ -37,5 +37,4 @@ val add_relation :
 val add_setoid : constr_expr -> constr_expr -> constr_expr -> unit
 
 val new_named_morphism :
- Names.identifier -> constr_expr ->
-  (morphism_argument list * constr_expr) option -> unit
+ Names.identifier -> constr_expr -> morphism_signature option -> unit