many checks guarded with if Utils.debug_metas

diff --git a/helm/software/components/tactics/paramodulation/founif.ml b/helm/software/components/tactics/paramodulation/founif.ml
index c2df6371c410fa8da7d18b9b6d296c6a1b0d8bb2..b635599515b75ba0d77fc7f6e7cbe793df66ee9a 100644 (file)
--- a/helm/software/components/tactics/paramodulation/founif.ml
+++ b/helm/software/components/tactics/paramodulation/founif.ml
@@ -206,9 +206,10 @@ let unification_aux b metasenv1 metasenv2 context t1 t2 ugraph =
   if Utils.debug_metas then
     ignore(check_for_duplicates menv "unification_aux prima di apply_subst");
   let menv = Subst.apply_subst_metasenv subst menv in
-  let _ = check_for_duplicates menv "unif_aux after" in
-    check_metasenv "unification_aux after 1" menv;
-    subst, menv, ug
+  if Utils.debug_metas then
+    (let _ = check_for_duplicates menv "unif_aux after" in
+    check_metasenv "unification_aux after 1" menv);
+  subst, menv, ug
 ;;
 
 exception MatchingFailure;;

diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml
index 97e45522d04cf83886b485c53bbeab8335d21272..99f66f1d11ccef7c114c5b4c0b93549c04641421 100644 (file)
--- a/helm/software/components/tactics/paramodulation/indexing.ml
+++ b/helm/software/components/tactics/paramodulation/indexing.ml
@@ -145,7 +145,7 @@ let not_unit_eq ctx eq =
   List.exists 
     (fun (_,_,ty) ->
        try 
-        let s,_ = CicTypeChecker.type_of_aux' metas ctx ty CicUniv.empty_ugraph
+        let s,_ = CicTypeChecker.type_of_aux' metas ctx ty CicUniv.oblivion_ugraph
         in s = Cic.Sort(Cic.Prop)
        with _ -> 
         prerr_endline ("ERROR typing " ^ CicPp.ppterm ty); assert false) metas
@@ -313,7 +313,8 @@ let rec find_matches bag metasenv context ugraph lift_amount term termty =
               Founif.matching 
                 metasenv metas context term (S.lift lift_amount c) ugraph
             in
-           check_metasenv "founif :" metasenv';
+            if Utils.debug_metas then
+             check_metasenv "founif :" metasenv';
             Some (Cic.Rel(1+lift_amount),subst',metasenv',ugraph',candidate)
           in
           let c, other =
@@ -517,7 +518,8 @@ let subsumption_aux_all use_unification env table target =
   let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
   let _, context, ugraph = env in
   let metasenv = tmetas in
-  check_for_duplicates metasenv "subsumption_aux_all";
+  if Utils.debug_metas then
+    check_for_duplicates metasenv "subsumption_aux_all";
   let predicate, unif_fun = 
     if use_unification then
       Unification, Founif.unification
@@ -576,12 +578,13 @@ let rec demodulation_aux bag ?from ?(typecheck=false)
   let module S = CicSubstitution in
   let module M = CicMetaSubst in
   let module HL = HelmLibraryObjects in
-  check_for_duplicates metasenv "in input a demodulation aux";
+  if Utils.debug_metas then
+    check_for_duplicates metasenv "in input a demodulation aux";
   let candidates = 
     get_candidates 
       ~env:(metasenv,context,ugraph) (* Unification *) Matching table term 
-  in let candidates = List.filter (fun _,x -> not (not_unit_eq context x)) candidates 
-  in
+  in 
+(*   let candidates = List.filter (fun _,x -> not (not_unit_eq context x)) candidates in *)
   let res =
     match term with
       | C.Meta _ -> None
@@ -899,8 +902,8 @@ let rec betaexpand_term
   | C.Meta (i, l) -> res, lifted_term
   | term ->
       let termty, ugraph =
-(*        C.Implicit None, ugraph *)
-         CicTypeChecker.type_of_aux' metasenv context term ugraph 
+       C.Implicit None, ugraph
+(*          CicTypeChecker.type_of_aux' metasenv context term ugraph  *)
       in
       let candidates = get_candidates Unification table term in
       (* List.iter (fun (_,e) -> debug_print (lazy (Equality.string_of_equality e))) candidates; *)

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index 8f4e5485174433bcbbb8b55b75610969d1620a76..7ee7d6b162d5f439b5fad8a45917bf57c9e3f75a 100644 (file)
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -820,7 +820,8 @@ let find_all_subsumed bag env table (goalproof,menv,ty) =
          (fun (subst, equality, swapped) (bag,acc) ->
             let (_,p,(ty,l,r,_),m,id) = Equality.open_equality equality in
              let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in
-             Indexing.check_for_duplicates cicmenv "from subsumption";
+             if Utils.debug_metas then
+               Indexing.check_for_duplicates cicmenv "from subsumption";
              let bag, p =
               if swapped then
                  Equality.symmetric bag eq_ty l id uri m