X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fextlib%2FpatternMatcher.ml;h=f57c3ea6cc82affc53668bdbf507fdde774be558;hb=bb246930370226dc96c9b9121f59853a0a2f1434;hp=c1b436a97cf241d120109b6b7357d179f2f27d5d;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/components/extlib/patternMatcher.ml b/matita/components/extlib/patternMatcher.ml
index c1b436a97..f57c3ea6c 100644
--- 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