This is only a temporary patch. The typecheker raises a

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

diff --git a/helm/software/components/tactics/paramodulation/equality_retrieval.ml b/helm/software/components/tactics/paramodulation/equality_retrieval.ml
index 886cc7ffe2e1ca03840279ea0d71d115d2c7cfd6..962304d41ac8d7c28df9dc9cfffebdd6242aac18 100644 (file)
--- a/helm/software/components/tactics/paramodulation/equality_retrieval.ml
+++ b/helm/software/components/tactics/paramodulation/equality_retrieval.ml
@@ -136,7 +136,7 @@ let equations_blacklist = UriManager.UriSet.empty;;
 (*****************************************************************)
 exception AutoFailure of AutoCache.cache * int
 
-let default_auto maxm _ _ _ _ _ = [],AutoCache.cache_empty,maxm ;; 
+let default_auto maxm _ _ _ c _ = [],c,maxm ;; 
 
 let close_hypothesis_of_term context metasenv oldnewmeta term cache auto fast = 
   let head, metasenv, args, newmeta =
@@ -210,10 +210,10 @@ let find_context_equalities
   let module T = CicTypeChecker in
   let _,metasenv,_,_ = proof in
   let newmeta = max (ProofEngineHelpers.new_meta_of_proof ~proof) maxmeta in
-  let use_auto, auto =
+  let auto =
     match auto with
-      | None -> false, default_auto
-      | Some auto -> true, auto in
+      | None -> default_auto
+      | Some auto -> auto in
   (* if use_auto is true, we try to close the hypothesis of equational
     statements using auto; a naif, and probably wrong approach *)
   let rec aux cache index newmeta = function
@@ -224,7 +224,7 @@ let find_context_equalities
              (Printf.sprintf "Examining: %d (%s)" index (CicPp.ppterm term)));
         let do_find context term =
           match term with
-          | C.Prod (name, s, t) when (is_an_equality t && use_auto) ->
+          | C.Prod (name, s, t) when is_an_equality t ->
               (try 
                 let term = S.lift index term in
                 let saturated,cache,newmeta = 
@@ -302,10 +302,10 @@ let find_library_equalities bag
  let candidates = List.map utty_of_u eqs in
  let candidates = List.filter is_monomorphic_eq candidates in
  let candidates = List.filter is_var_free candidates in
- let use_auto, auto =
+ let auto =
     match auto with
-      | None -> false, default_auto
-      | Some auto -> true, auto in
+      | None -> default_auto
+      | Some auto -> auto in
   (* if use_auto is true, we try to close the hypothesis of equational
     statements using auto; a naif, and probably wrong approach *)
  let rec aux cache newmeta = function
@@ -317,7 +317,7 @@ let find_library_equalities bag
                 (CicPp.ppterm term) (CicPp.ppterm termty)));
         let res, newmeta, cache = 
           match termty with
-          | C.Prod (name, s, t) when use_auto ->
+          | C.Prod (name, s, t) ->
               (try
                 let saturated,cache,newmeta = 
                   close_hypothesis_of_term context metasenv newmeta termty 
@@ -341,7 +341,6 @@ let find_library_equalities bag
                  eqs, newmeta , cache
                with AutoFailure (cache,newmeta) ->
                 [], newmeta , cache)
-          | C.Prod _ ->  [], newmeta, cache
           | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] -> 
               let newmeta, e = build_equality bag ty t1 t2 term [] newmeta in
               [e], newmeta+1, cache