From 15010cea58df81a3ccfdd5a4b2a01375e34853f3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 18 Jun 2018 16:43:42 +0200
Subject: Do not rely on the Ident vs. Qualid artificial separation.

---
 src/tac2core.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'src/tac2core.ml')

diff --git a/src/tac2core.ml b/src/tac2core.ml
index 5f33374486..4bd294d4df 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -910,13 +910,14 @@ let () =
   define_ml_object Tac2quote.wit_pattern obj
 
 let () =
-  let intern self ist qid = match qid with
-  | {CAst.v=Libnames.Ident id} ->
+  let intern self ist ref = match ref.CAst.v with
+  | Tac2qexpr.QHypothesis id ->
     GlbVal (Globnames.VarRef id), gtypref t_reference
-  | {CAst.loc;v=Libnames.Qualid qid} ->
+  | Tac2qexpr.QReference qid ->
     let gr =
       try Nametab.locate qid
       with Not_found ->
+        let loc = ref.CAst.loc in
         Nametab.error_global_not_found (CAst.make ?loc qid)
     in
     GlbVal gr, gtypref t_reference
-- 
cgit v1.2.3