diff options
Diffstat (limited to 'src/tac2core.ml')
| -rw-r--r-- | src/tac2core.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/src/tac2core.ml b/src/tac2core.ml index 4bd294d4df..97f25ef5ed 100644 --- a/src/tac2core.ml +++ b/src/tac2core.ml @@ -917,8 +917,7 @@ let () = let gr = try Nametab.locate qid with Not_found -> - let loc = ref.CAst.loc in - Nametab.error_global_not_found (CAst.make ?loc qid) + Nametab.error_global_not_found qid in GlbVal gr, gtypref t_reference in |