diff options
| author | Pierre-Marie Pédrot | 2016-10-17 18:09:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-10-17 18:09:28 +0200 |
| commit | 1929b52db6bc282c60a1a3aa39ba87307c68bf78 (patch) | |
| tree | 57a6c7632dec646afb3ab6a1a9519eb313e805ac /interp | |
| parent | 05ad4f49ac2203dd64dfec79a1fc62ee52115724 (diff) | |
| parent | 34b1813b5adf1df556e0d8a05bde0ec58152f610 (diff) | |
Merge branch 'v8.6'
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 11 | ||||
| -rw-r--r-- | interp/notation.ml | 3 | ||||
| -rw-r--r-- | interp/notation.mli | 3 |
3 files changed, 7 insertions, 10 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 4aff82403e..3077231be0 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -149,17 +149,8 @@ let extern_evar loc n l = CEvar (loc,n,l) For instance, in the debugger the tables of global references may be inaccurate *) -let safe_shortest_qualid_of_global vars r = - try shortest_qualid_of_global vars r - with Not_found -> - match r with - | VarRef v -> make_qualid DirPath.empty v - | ConstRef c -> make_qualid DirPath.empty Names.(Label.to_id (con_label c)) - | IndRef (i,_) | ConstructRef ((i,_),_) -> - make_qualid DirPath.empty Names.(Label.to_id (mind_label i)) - let default_extern_reference loc vars r = - Qualid (loc,safe_shortest_qualid_of_global vars r) + Qualid (loc,shortest_qualid_of_global vars r) let my_extern_reference = ref default_extern_reference diff --git a/interp/notation.ml b/interp/notation.ml index 1bd1bc7d5d..948d624a27 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -1012,6 +1012,9 @@ let find_notation_parsing_rules ntn = try pi3 (String.Map.find ntn !notation_rules) with Not_found -> anomaly (str "No parsing rule found for " ++ str ntn) +let get_defined_notations () = + String.Set.elements @@ String.Map.domain !notation_rules + let add_notation_extra_printing_rule ntn k v = try notation_rules := diff --git a/interp/notation.mli b/interp/notation.mli index b47e1975e3..2e92a00a8c 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -203,6 +203,9 @@ val find_notation_extra_printing_rules : notation -> extra_unparsing_rules val find_notation_parsing_rules : notation -> notation_grammar val add_notation_extra_printing_rule : notation -> string -> string -> unit +(** Returns notations with defined parsing/printing rules *) +val get_defined_notations : unit -> notation list + (** Rem: printing rules for primitive token are canonical *) val with_notation_protection : ('a -> 'b) -> 'a -> 'b |