Compiled with recent OCaml, Matita now fails removing
a notation when it starts. The patch avoids the assert
false. I have not investigated what's going on.
[InterpretationId interp_id]
| st -> []
[InterpretationId interp_id]
| st -> []
+(* CSC: Matita compiled with recent OCaml triggers the assert false in the
+ code below. The exception FOO trick ignores the failure. It seems to
+ work, but it's the classical patch without understanding what the problem
+ is. *)
+exception FOO;;
+
let remove_notation = function
let remove_notation = function
+xxx -> try match xxx with
| RuleId id ->
let item =
try
Hashtbl.find !rule_ids_to_items id
| RuleId id ->
let item =
try
Hashtbl.find !rule_ids_to_items id
- with Not_found -> assert false in
+ with Not_found -> raise FOO (*assert false*) in
RefCounter.decr ~delete_cb:(fun _ -> CicNotationParser.delete id)
!parser_ref_counter item
| PrettyPrinterId id -> TermContentPres.remove_pretty_printer id
| InterpretationId id -> TermAcicContent.remove_interpretation id
RefCounter.decr ~delete_cb:(fun _ -> CicNotationParser.delete id)
!parser_ref_counter item
| PrettyPrinterId id -> TermContentPres.remove_pretty_printer id
| InterpretationId id -> TermAcicContent.remove_interpretation id
let get_all_notations () =
List.map
let get_all_notations () =
List.map