diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-20 23:10:08 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-20 23:10:08 +0000 |
| commit | 9e1855ccee6e39a4b73fead883be5c92f301412a (patch) | |
| tree | f74b48d31b369913b8ea3e2f3b96edc583a840c9 /toplevel | |
| parent | 1f96d480842a1206a9334d0c8b1b6cc4647066ef (diff) | |
Correction bug affichage Infix/Distfix
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2036 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -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 3094fbacb..39e74dc44 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1445,7 +1445,7 @@ let _ = add "INFIX" (function | [VARG_AST assoc; VARG_NUMBER n; VARG_STRING inf; VARG_QUALID pref] -> - let ref = Termast.ast_of_qualid pref in + let ref = Termast.ast_of_ref (locate_qualid dummy_loc pref) in (fun () -> Metasyntax.add_infix (Extend.gram_assoc assoc) n inf ref) | _ -> bad_vernac_args "INFIX") @@ -1454,7 +1454,7 @@ let _ = add "DISTFIX" (function | [VARG_AST assoc; VARG_NUMBER n; VARG_STRING s; VARG_QUALID pref] -> - let ref = Termast.ast_of_qualid pref in + let ref = Termast.ast_of_ref (locate_qualid dummy_loc pref) in (fun () -> Metasyntax.add_distfix (Extend.gram_assoc assoc) n s ref) | _ -> bad_vernac_args "DISTFIX") |