Trivial bug in equality_replace fixed: an exception was raised in spite of

returning false.

diff --git a/helm/gTopLevel/proofEngineReduction.ml b/helm/gTopLevel/proofEngineReduction.ml
index 265e5f99ceb37049618a27e6c86e07c363ea60fd..442873cecb17dba0f22aa7f66049025132a800ae 100644 (file)
--- a/helm/gTopLevel/proofEngineReduction.ml
+++ b/helm/gTopLevel/proofEngineReduction.ml
@@ -73,7 +73,11 @@ let rec syntactic_equality t t' =
         syntactic_equality s s' &&
          syntactic_equality t t'
     | C.Appl l, C.Appl l' ->
-       List.fold_left2 (fun b t1 t2 -> b && syntactic_equality t1 t2) true l l'
+       (try
+         List.fold_left2
+          (fun b t1 t2 -> b && syntactic_equality t1 t2) true l l'
+        with
+         Invalid_argument _ -> false)
     | C.Const (uri,_), C.Const (uri',_) -> UriManager.eq uri uri'
     | C.MutInd (uri,_,i), C.MutInd (uri',_,i') ->
        UriManager.eq uri uri' && i = i'
@@ -83,22 +87,31 @@ let rec syntactic_equality t t' =
        UriManager.eq sp sp' && i = i' &&
         syntactic_equality outt outt' &&
          syntactic_equality t t' &&
-          List.fold_left2
-           (fun b t1 t2 -> b && syntactic_equality t1 t2) true pl pl'
+          (try
+            List.fold_left2
+             (fun b t1 t2 -> b && syntactic_equality t1 t2) true pl pl'
+           with
+            Invalid_argument _ -> false)
     | C.Fix (i,fl), C.Fix (i',fl') ->
        i = i' &&
-        List.fold_left2
-         (fun b (name,i,ty,bo) (name',i',ty',bo') ->
-           b && name = name' && i = i' &&
-            syntactic_equality ty ty' &&
-             syntactic_equality bo bo') true fl fl'
+       (try
+         List.fold_left2
+          (fun b (name,i,ty,bo) (name',i',ty',bo') ->
+            b && name = name' && i = i' &&
+             syntactic_equality ty ty' &&
+              syntactic_equality bo bo') true fl fl'
+        with
+         Invalid_argument _ -> false)
     | C.CoFix (i,fl), C.CoFix (i',fl') ->
        i = i' &&
-        List.fold_left2
-         (fun b (name,ty,bo) (name',ty',bo') ->
-           b && name = name' &&
-            syntactic_equality ty ty' &&
-             syntactic_equality bo bo') true fl fl'
+       (try
+         List.fold_left2
+          (fun b (name,ty,bo) (name',ty',bo') ->
+            b && name = name' &&
+             syntactic_equality ty ty' &&
+              syntactic_equality bo bo') true fl fl'
+        with
+         Invalid_argument _ -> false)
     | _,_ -> false
 ;;
 
@@ -152,6 +165,7 @@ let replace_lifting ~equality ~what ~with_what ~where =
  let rec substaux k =
   let module C = Cic in
    function
+(*CSC: Possibile bug: debbo liftare di k what? *)
       t when (equality t what) -> CicSubstitution.lift (k-1) with_what
     | C.Rel n as t -> t (*CSC: ??? BUG ? *)
     | C.Var _ as t  -> t