diff options
| author | barras | 2001-03-09 16:11:48 +0000 |
|---|---|---|
| committer | barras | 2001-03-09 16:11:48 +0000 |
| commit | 36701f1900c8247d76436f2cf7ee09865b45ce3f (patch) | |
| tree | 676be76a6456ac80de184f3f9573fb68682aa583 /toplevel/metasyntax.ml | |
| parent | ba343a917c0871a60669e5e95c63a9ed9b796ba4 (diff) | |
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
Diffstat (limited to 'toplevel/metasyntax.ml')
| -rw-r--r-- | toplevel/metasyntax.ml | 12 |
1 files changed, 5 insertions, 7 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index d95e254c88..c567a2f94a 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -224,11 +224,10 @@ let add_infix assoc n inf pr = errorlabstrm "Vernacentries.infix_grammar_entry" [< 'sTR"Associativity Precedence must be 6,7,8 or 9." >]; (* check the grammar entry *) - let prefast = Termast.ast_of_ref pr in - let prefname = (Names.string_of_path (Global.sp_of_global pr))^"_infix" in - let gram_rule = gram_infix assoc n (split inf) prefname prefast in + let prefname = inf^"_infix" in + let gram_rule = gram_infix assoc n (split inf) prefname pr in (* check the syntax entry *) - let syntax_rule = infix_syntax_entry assoc n inf prefname prefast in + let syntax_rule = infix_syntax_entry assoc n inf prefname pr in Lib.add_anonymous_leaf (inInfix(gram_rule,syntax_rule)) (* Distfix *) @@ -272,8 +271,7 @@ let distfix assoc n sl fname astf = ] } -let add_distfix a n df f = - let fname = (Names.string_of_path (Global.sp_of_global f))^"_distfix" in - let astf = Termast.ast_of_ref f in +let add_distfix a n df astf = + let fname = df^"_distfix" in Lib.add_anonymous_leaf (inInfix(distfix a n (split df) fname astf, [])) |