diff options
Diffstat (limited to 'interp/smartlocate.ml')
| -rw-r--r-- | interp/smartlocate.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml index 64d260cc1..fd9599ec0 100644 --- a/interp/smartlocate.ml +++ b/interp/smartlocate.ml @@ -67,14 +67,14 @@ let smart_global ?head = function | AN r -> global_with_alias ?head r | ByNotation (loc,(ntn,sc)) -> - Notation.interp_notation_as_global_reference loc (fun _ -> true) ntn sc + Notation.interp_notation_as_global_reference ~loc (fun _ -> true) ntn sc let smart_global_inductive = function | AN r -> global_inductive_with_alias r | ByNotation (loc,(ntn,sc)) -> destIndRef - (Notation.interp_notation_as_global_reference loc isIndRef ntn sc) + (Notation.interp_notation_as_global_reference ~loc isIndRef ntn sc) let loc_of_smart_reference = function | AN r -> loc_of_reference r |