From 36701f1900c8247d76436f2cf7ee09865b45ce3f Mon Sep 17 00:00:00 2001
From: barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 9 Mar 2001 16:11:48 +0000
Subject: protection contre certaines exceptions levees par marshal_{in,out}
 possibilite de declarer une def syntaxique comme infix (utilise par FTA)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1442 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/metasyntax.mli | 10 ++--------
 1 file changed, 2 insertions(+), 8 deletions(-)

(limited to 'toplevel/metasyntax.mli')

diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index 08fb2800d..b51a9a43d 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -1,12 +1,6 @@
 
 (*i $Id$ i*)
 
-(*i*)
-open Extend
-open Names
-open Term
-(*i*)
-
 (* Adding grammar and pretty-printing objects in the environment *)
 
 val add_syntax_obj : string -> Coqast.t list -> unit
@@ -15,8 +9,8 @@ val add_grammar_obj : string -> Coqast.t list -> unit
 val add_token_obj : string -> unit
 
 val add_infix :
-  Gramext.g_assoc option -> int -> string -> global_reference -> unit
+  Gramext.g_assoc option -> int -> string -> Coqast.t -> unit
 val add_distfix :
-  Gramext.g_assoc option -> int -> string -> global_reference -> unit
+  Gramext.g_assoc option -> int -> string -> Coqast.t -> unit
 
 val print_grammar : string -> string -> unit
-- 
cgit v1.2.3