From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 28 Dec 2017 20:09:15 +0000 (+0100)
Subject: Horrible workaround
X-Git-Tag: make_still_working~382
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e83cd27fc0694c34baf35c8b80d32317e51be707;p=helm.git

Horrible workaround

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.
---

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