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/tac2core.ml | |
| parent | 1bbeba35eb385f813a0e4b6d25a437f9bab8191b (diff) | |
Do not rely on the Ident vs. Qualid artificial separation.
Diffstat (limited to 'src/tac2core.ml')
| -rw-r--r-- | src/tac2core.ml | 7 |
1 files changed, 4 insertions, 3 deletions
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 |