From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 17 Jun 2011 11:32:30 +0000 (+0000)
Subject: Unprotected List.fold_left2.
X-Git-Tag: make_still_working~2430
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3a3517f9a23d9344ff6461e76e1c6c429d44db57;p=helm.git

Unprotected List.fold_left2.
---

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 =