From c1a05dd1556d2cd43a16efbd9a9250fea3314924 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 23 Oct 2000 17:33:04 +0000
Subject: Import de Infix au Require

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@743 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/metasyntax.ml | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index f9b315842e..ce7c4f1d05 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -106,16 +106,17 @@ let split str =
 
 (* An infix or a distfix is a pair of a grammar rule and a pretty-printing rule
  *)
+let cache_infix (_,(gr,se)) =
+  Egrammar.extend_grammar gr;
+  Esyntax.add_ppobject {sc_univ="constr";sc_entries=se}
+
 let (inInfix, outInfix) =
   declare_object
     ("INFIX",
-     { load_function = (fun _ -> ());
+     { load_function = cache_infix;
        open_function = (fun _ -> ());
-       cache_function =
-	 (fun (_,(gr,se)) ->
-            Egrammar.extend_grammar gr;
-            Esyntax.add_ppobject {sc_univ="constr";sc_entries=se});
-     specification_function = (fun x -> x)})
+       cache_function = cache_infix;
+       specification_function = (fun x -> x)})
 
 let prec_assoc = function
   | Some(Gramext.RightA) -> (":L",":E")
-- 
cgit v1.2.3