X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Flexicon%2FcicNotation.ml;h=29c4f0e5d79547c562a1c6cefe196b669cd9ed25;hb=e83cd27fc0694c34baf35c8b80d32317e51be707;hp=ebc9463ee6b457ed8ae3395d419f13c3872c7440;hpb=1d3dc48a9755b08ecb93d88b67b8445fbb314ad6;p=helm.git

diff --git a/helm/software/components/lexicon/cicNotation.ml b/helm/software/components/lexicon/cicNotation.ml
index ebc9463ee..29c4f0e5d 100644
--- 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