From 9e1855ccee6e39a4b73fead883be5c92f301412a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 20 Sep 2001 23:10:08 +0000
Subject: Correction bug affichage Infix/Distfix

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2036 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/vernacentries.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 3094fbacbb..39e74dc44c 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")
-- 
cgit v1.2.3