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 2b963e94e410e1307f219cdd10ca7dfacd20cd33..29c4f0e5d79547c562a1c6cefe196b669cd9ed25 100644 (file)
--- a/helm/software/components/lexicon/cicNotation.ml
+++ b/helm/software/components/lexicon/cicNotation.ml
@@ -49,7 +49,8 @@ let process_notation st =
   match st with
   | Notation (loc, dir, l1, associativity, precedence, l2) ->
       let l1 = 
-        CicNotationParser.check_l1_pattern l1 precedence associativity
+        CicNotationParser.check_l1_pattern
+         l1 (dir = Some `RightToLeft) precedence associativity
       in
       let item = (l1, precedence, associativity, l2) in
       let rule_id = ref [] in
@@ -80,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