the case Appl Meta vs t was not executed in case t was a Constant,Mutcase,Cofix,Fix...

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index 7a67c8248e4e5d72d7986166cd5ec9f5401213cc..dc7cd2721b91d02ea0bb8dd31aacf536312654de 100644 (file)
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -540,6 +540,20 @@ debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (strin
              "Can't unify %s with %s because they are not convertible"
              (CicMetaSubst.ppterm subst t1) 
              (CicMetaSubst.ppterm subst t2))) *)
+   | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
+       let subst,metasenv,beta_expanded,ugraph1 =
+         beta_expand_many 
+           test_equality_only metasenv subst context t2 args ugraph 
+       in
+         fo_unif_subst test_equality_only subst context metasenv 
+           (C.Meta (i,l)) beta_expanded ugraph1
+   | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
+       let subst,metasenv,beta_expanded,ugraph1 =
+         beta_expand_many 
+           test_equality_only metasenv subst context t1 args ugraph 
+       in
+         fo_unif_subst test_equality_only subst context metasenv 
+           beta_expanded (C.Meta (i,l)) ugraph1
    | (C.Sort _ ,_) | (_, C.Sort _)
    | (C.Const _, _) | (_, C.Const _)
    | (C.MutInd  _, _) | (_, C.MutInd _)
@@ -557,23 +571,9 @@ debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (strin
            else
              raise (* (UnificationFailure "7") *)
                 (UnificationFailure (sprintf
-                  "Can't unify %s with %s because they are not convertible"
+                  "7: Can't unify %s with %s because they are not convertible"
                   (CicMetaSubst.ppterm subst t1) 
                   (CicMetaSubst.ppterm subst t2)))
-   | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
-       let subst,metasenv,beta_expanded,ugraph1 =
-         beta_expand_many 
-           test_equality_only metasenv subst context t2 args ugraph 
-       in
-         fo_unif_subst test_equality_only subst context metasenv 
-           (C.Meta (i,l)) beta_expanded ugraph1
-   | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
-       let subst,metasenv,beta_expanded,ugraph1 =
-         beta_expand_many 
-           test_equality_only metasenv subst context t1 args ugraph 
-       in
-         fo_unif_subst test_equality_only subst context metasenv 
-           beta_expanded (C.Meta (i,l)) ugraph1
    | (C.Prod _, t2) ->
        let t2' = R.whd ~subst context t2 in
        (match t2' with
@@ -590,7 +590,7 @@ debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (strin
           | _ -> (* raise (UnificationFailure "9")) *)
              raise 
                 (UnificationFailure (sprintf
-                   "Can't unify %s with %s because they are not convertible"
+                   "9: Can't unify %s with %s because they are not convertible"
                    (CicMetaSubst.ppterm subst t1) 
                    (CicMetaSubst.ppterm subst t2))))
    | (_,_) ->