From 3a3517f9a23d9344ff6461e76e1c6c429d44db57 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 17 Jun 2011 11:32:30 +0000 Subject: [PATCH] Unprotected List.fold_left2. --- matita/components/ng_tactics/nTacStatus.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/matita/components/ng_tactics/nTacStatus.ml b/matita/components/ng_tactics/nTacStatus.ml index 143aac98e..99c35d7ff 100644 --- a/matita/components/ng_tactics/nTacStatus.ml +++ b/matita/components/ng_tactics/nTacStatus.ml @@ -397,7 +397,7 @@ let select_term let ctx = (n, NCic.Decl s2) :: ctx in let status, t = select status ctx t1 t2 in status, NCic.Prod (n,s,t) - | NCic.Appl l1, NCic.Appl l2 -> + | NCic.Appl l1, NCic.Appl l2 when List.length l1 = List.length l2 -> let status, l = List.fold_left2 (fun (status,l) x y -> @@ -406,7 +406,8 @@ let select_term (status,[]) l1 l2 in status, NCic.Appl (List.rev l) - | NCic.Match (_,ot1,t1,pl1), NCic.Match (u,ot2,t2,pl2) -> + | NCic.Match (_,ot1,t1,pl1), NCic.Match (u,ot2,t2,pl2) + when List.length pl1 = List.length pl2 -> let status, t = select status ctx t1 t2 in let status, ot = select status ctx ot1 ot2 in let status, pl = -- 2.39.2