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/tac2qexpr.mli | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

(limited to 'src/tac2qexpr.mli')

diff --git a/src/tac2qexpr.mli b/src/tac2qexpr.mli
index 3f0c591e63..400ab1a092 100644
--- a/src/tac2qexpr.mli
+++ b/src/tac2qexpr.mli
@@ -16,6 +16,12 @@ type 'a or_anti =
 | QExpr of 'a
 | QAnti of Id.t CAst.t
 
+type reference_r =
+| QReference of Libnames.qualid
+| QHypothesis of Id.t
+
+type reference = reference_r CAst.t
+
 type quantified_hypothesis =
 | QAnonHyp of int CAst.t
 | QNamedHyp of Id.t CAst.t
@@ -116,8 +122,8 @@ type red_flag_r =
 | QFix
 | QCofix
 | QZeta
-| QConst of Libnames.reference or_anti list CAst.t
-| QDeltaBut of Libnames.reference or_anti list CAst.t
+| QConst of reference or_anti list CAst.t
+| QDeltaBut of reference or_anti list CAst.t
 
 type red_flag = red_flag_r CAst.t
 
-- 
cgit v1.2.3