From: Andrea Asperti Date: Fri, 20 Oct 2006 14:37:25 +0000 (+0000) Subject: The function exists_a_meta has been modified to capture also X-Git-Tag: 0.4.95@7852~870 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5919a51b69b776dfc03cf44fab30263e232ef5f1;p=helm.git The function exists_a_meta has been modified to capture also flexible arguments instead of metas. --- diff --git a/components/cic_unification/cicUnification.ml b/components/cic_unification/cicUnification.ml index 6004e73fa..8ba0ae917 100644 --- a/components/cic_unification/cicUnification.ml +++ b/components/cic_unification/cicUnification.ml @@ -74,7 +74,11 @@ in profiler_toa.HExtlib.profile foo () ;; let exists_a_meta l = - List.exists (function Cic.Meta _ -> true | _ -> false) l + List.exists + (function + | Cic.Meta _ + | Cic.Appl (Cic.Meta _::_) -> true + | _ -> false) l let rec deref subst t = let snd (_,a,_) = a in @@ -655,7 +659,9 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ C.Appl (C.MutInd _::_) -> fo_unif_subst test_equality_only subst context metasenv t1 t2' ugraph - | _ -> raise (UnificationFailure (lazy "99"))) + | _ -> raise + (UnificationFailure + (lazy ("not a mutind :"^CicMetaSubst.ppterm subst t2 )))) | _ -> raise exn))) | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))-> let subst', metasenv',ugraph1 =