diff options
| author | Enrico Tassi | 2014-07-14 12:44:32 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2014-07-14 12:48:33 +0200 |
| commit | 8e328c6c3b2d6cfe3110abdfe5bb57eeba9c0cc4 (patch) | |
| tree | 03e9e4c6cdc662b66b7f97670af051793869e765 /toplevel | |
| parent | 99cee0e8d64567c6a89ab665c6e4dfd934674142 (diff) | |
smartlocate: look for the head symbol for real
This bug was hacked around in ssreflect, but with the new idea
that parsing and interpretation are done in distinct phases the
work around could not be implemented anymore.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index b98801ea7d..074d260c74 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -42,7 +42,7 @@ let prerr_endline = let cl_of_qualid = function | FunClass -> Classops.CL_FUN | SortClass -> Classops.CL_SORT - | RefClass r -> Class.class_of_global (Smartlocate.smart_global r) + | RefClass r -> Class.class_of_global (Smartlocate.smart_global ~head:true r) let scope_class_of_qualid qid = Notation.scope_class_of_reference (Smartlocate.smart_global qid) |