Not well understood patch: an assert false did occur, so I changed it to a

pattern matching failure. However, I do not know if this was due to a badly
defined notation or not.

diff --git a/matita/components/extlib/patternMatcher.ml b/matita/components/extlib/patternMatcher.ml
index c1b436a97cf241d120109b6b7357d179f2f27d5d..f57c3ea6cc82affc53668bdbf507fdde774be558 100644 (file)
--- a/matita/components/extlib/patternMatcher.ml
+++ b/matita/components/extlib/patternMatcher.ml
@@ -113,12 +113,12 @@ struct
         | _ -> assert false)
       t
 
-  let variable_closure ksucc =
+  let variable_closure ksucc kfail =
     (fun matched_terms constructors terms ->
 (* prerr_endline "variable_closure"; *)
       match terms with
       | hd :: tl -> ksucc (hd :: matched_terms) constructors tl
-      | _ -> assert false)
+      | _ -> kfail () (*CSC: was assert false, but it did happen*))
 
   let success_closure ksucc =
     (fun matched_terms constructors terms ->
@@ -156,7 +156,7 @@ struct
       else
         match horizontal_split t with
         | _, [], _ -> assert false
-        | Variable, t', [] -> variable_closure (aux (vertical_split t'))
+        | Variable, t', [] -> variable_closure (aux (vertical_split t')) fail_k
         | Constructor, t', [] ->
             let tagl =
               List.map