From cab46a693418cb8a797bcaf8bb026dc1ba9b32d6 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 27 Nov 2006 12:42:03 +0000 Subject: [PATCH] Commented a few assertions. --- components/tactics/paramodulation/indexing.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml index 28c22a64e..b535119ed 100644 --- a/components/tactics/paramodulation/indexing.ml +++ b/components/tactics/paramodulation/indexing.ml @@ -655,7 +655,7 @@ let rec demodulation_equality bag ?from eq_uri newmeta env table target = match res with | Some t -> let newmeta, newtarget = build_newtarget true t in - assert (not (Equality.meta_convertibility_eq target newtarget)); + (* assert (not (Equality.meta_convertibility_eq target newtarget)); *) if (Equality.is_weak_identity newtarget) (* || *) (*Equality.meta_convertibility_eq target newtarget*) then newmeta, newtarget @@ -959,7 +959,7 @@ let rec demodulation_theorem bag newmeta env table theorem = let open_goal g = match g with | (proof,menv,Cic.Appl[(Cic.MutInd(uri,0,_)) as eq;ty;l;r]) -> - assert (LibraryObjects.is_eq_URI uri); + (* assert (LibraryObjects.is_eq_URI uri); *) proof,menv,eq,ty,l,r | _ -> assert false ;; -- 2.39.2