diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-23 17:33:04 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-23 17:33:04 +0000 |
| commit | c1a05dd1556d2cd43a16efbd9a9250fea3314924 (patch) | |
| tree | 7ac6d7c3e4dbc4de16d491e7de82456f8807e2dc /toplevel/metasyntax.ml | |
| parent | a128c458a62cd86a6ff3bea5b5a4e20e8e792f26 (diff) | |
Import de Infix au Require
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@743 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/metasyntax.ml')
| -rw-r--r-- | toplevel/metasyntax.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index f9b315842..ce7c4f1d0 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") |