From 5b14f117bbaba498168de06ad0617d67741a6d17 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 26 Sep 2011 12:24:20 +0000 Subject: [PATCH] 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. --- matita/components/extlib/patternMatcher.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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 -- 2.39.2