many checks guarded with if Utils.debug_metas

[helm.git] / helm / software / components / tactics / paramodulation / indexing.ml

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; *)