From afa14a92f2a1fbc1c3b40298ddc77a0c7413857d Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 27 Nov 2006 12:52:53 +0000 Subject: [PATCH] Commented an assertion. --- components/tactics/paramodulation/founif.ml | 2 -- 1 file changed, 2 deletions(-) diff --git a/components/tactics/paramodulation/founif.ml b/components/tactics/paramodulation/founif.ml index ac80099b0..2a9de5ffa 100644 --- a/components/tactics/paramodulation/founif.ml +++ b/components/tactics/paramodulation/founif.ml @@ -106,9 +106,7 @@ let unification_simple locked_menv metasenv context t1 t2 ugraph = | C.Meta (i, l), t -> ( try let _, _, ty = CicUtil.lookup_meta i menv in - assert (not (Subst.is_in_subst i subst)); let subst = Subst.buildsubst i context t ty subst in - let menv = menv in (* List.filter (fun (m, _, _) -> i <> m) menv in *) subst, menv with CicUtil.Meta_not_found m -> let names = names_of_context context in -- 2.39.2