diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-21 12:42:43 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-21 12:42:43 +0000 |
| commit | a948eba3894f8b5351c208e4d12d27ba2902a54f (patch) | |
| tree | e9237c7f64506c2aa5205f15f9f449fd21ddab55 /toplevel/vernacentries.ml | |
| parent | 1eb7cdecb23bb4015c0ae3171e46b5879b60f26f (diff) | |
Mise en place globalisation optionnelle pour Infix/Distfix
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2046 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 420a4bf02..201896d90 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1449,7 +1449,7 @@ let _ = add "INFIX" (function | [VARG_AST assoc; VARG_NUMBER n; VARG_STRING inf; VARG_QUALID pref] -> - let ref = Termast.ast_of_ref (locate_qualid dummy_loc pref) in + let ref = Astterm.globalize_qualid pref in (fun () -> Metasyntax.add_infix (Extend.gram_assoc assoc) n inf ref) | _ -> bad_vernac_args "INFIX") @@ -1458,7 +1458,7 @@ let _ = add "DISTFIX" (function | [VARG_AST assoc; VARG_NUMBER n; VARG_STRING s; VARG_QUALID pref] -> - let ref = Termast.ast_of_ref (locate_qualid dummy_loc pref) in + let ref = Astterm.globalize_qualid pref in (fun () -> Metasyntax.add_distfix (Extend.gram_assoc assoc) n s ref) | _ -> bad_vernac_args "DISTFIX") |