From 22fca01c06d1b57068ec0c904c81474fa83edadf Mon Sep 17 00:00:00 2001
From: sacerdot
Date: Fri, 24 Sep 2004 20:21:39 +0000
Subject: New: (temporary) concrete syntax to specify the morphism signature:

 "Add Morphism m @ arg1 ... argn @ out as ident"

where argi = constr arrow
and arrow =  "-->" | "++>" | "==>" (for contravariant, covariant and
 bi-variant morphisms).

The syntax should be improved by getting rid of the "@" and maybe choosing
better symbols to represent the arrows.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6129 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/setoid_replace.mli | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'tactics/setoid_replace.mli')

diff --git a/tactics/setoid_replace.mli b/tactics/setoid_replace.mli
index a763f237ae..babd89f1a8 100644
--- a/tactics/setoid_replace.mli
+++ b/tactics/setoid_replace.mli
@@ -13,6 +13,10 @@ open Proof_type
 open Topconstr
 
 
+type morphism_argument = bool option * constr_expr
+
+val pr_morphism_argument : morphism_argument -> Pp.std_ppcmds
+
 val register_replace : (constr -> constr -> tactic) -> unit
 
 val print_setoids : unit -> unit
@@ -34,4 +38,4 @@ val add_setoid : constr_expr -> constr_expr -> constr_expr -> unit
 
 val new_named_morphism :
  Names.identifier -> constr_expr ->
-  ((bool option * constr_expr) list * constr_expr) option -> unit
+  (morphism_argument list * constr_expr) option -> unit
-- 
cgit v1.2.3