Horrible workaround

[helm.git] / helm / software / components / lexicon / cicNotation.ml

diff --git a/helm/software/components/lexicon/cicNotation.ml b/helm/software/components/lexicon/cicNotation.ml
index ebc9463ee6b457ed8ae3395d419f13c3872c7440..29c4f0e5d79547c562a1c6cefe196b669cd9ed25 100644 (file)
--- a/helm/software/components/lexicon/cicNotation.ml
+++ b/helm/software/components/lexicon/cicNotation.ml
@@ -81,16 +81,24 @@ let process_notation 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
+xxx -> try match xxx with
   | 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
+with FOO -> ();;
 
 let get_all_notations () =
   List.map