From: Enrico Tassi Date: Fri, 9 Sep 2005 13:03:25 +0000 (+0000) Subject: the case Appl Meta vs t was not executed in case t was a Constant,Mutcase,Cofix,Fix... X-Git-Tag: V_0_1_2_1~51 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3a12950125e7a4a792546aacea40505f3cecae89;p=helm.git the case Appl Meta vs t was not executed in case t was a Constant,Mutcase,Cofix,Fix,.... (I guess only if it was a Rel/Meta). --- diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index 7a67c8248..dc7cd2721 100644 --- 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)))) | (_,_) ->