From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 26 Sep 2011 12:24:20 +0000 (+0000)
Subject: Not well understood patch: an assert false did occur, so I changed it to a
X-Git-Tag: make_still_working~2268
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5b14f117bbaba498168de06ad0617d67741a6d17;p=helm.git

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