diff options
| author | Pierre-Marie Pédrot | 2018-06-18 16:43:42 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-06-18 17:00:02 +0200 |
| commit | 15010cea58df81a3ccfdd5a4b2a01375e34853f3 (patch) | |
| tree | 49070bb62f93b0aa00cd8ef78efc1bd1a3cc5ec5 /src/tac2qexpr.mli | |
| parent | 1bbeba35eb385f813a0e4b6d25a437f9bab8191b (diff) | |
Do not rely on the Ident vs. Qualid artificial separation.
Diffstat (limited to 'src/tac2qexpr.mli')
| -rw-r--r-- | src/tac2qexpr.mli | 10 |
1 files changed, 8 insertions, 2 deletions
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 |