From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 27 Jun 2006 16:54:28 +0000 (+0000)
Subject: using the new metadataConstraint function
X-Git-Tag: 0.4.95@7852~1274
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3b13c77858049d1ba3e206baa37b3135ab075848;p=helm.git

using the new metadataConstraint function
---

diff --git a/components/tactics/autoTactic.ml b/components/tactics/autoTactic.ml
index 63dc8631d..d4dc5592c 100644
--- a/components/tactics/autoTactic.ml
+++ b/components/tactics/autoTactic.ml
@@ -331,6 +331,7 @@ let auto_tac ~params ~(dbd:HMysql.dbd) =
   let target = string "target" params in
   let table = string "table" params in
   let subterms_only = bool "subterms_only" params in
+  let caso_strano = bool "caso_strano" params in
   let demod_table = string "demod_table" params in
   (* the real tactic *)
   let auto_tac dbd (proof, goal) =
@@ -363,7 +364,7 @@ let auto_tac ~params ~(dbd:HMysql.dbd) =
       debug_print (lazy "USO PARAMODULATION...");
 (*       try *)
       try
-        let rc = Saturation.saturate dbd ~depth ~width ~full (proof, goal) in
+        let rc = Saturation.saturate caso_strano dbd ~depth ~width ~full (proof, goal) in
         prerr_endline (Saturation.get_stats ());
         rc
       with exn ->
@@ -412,7 +413,7 @@ let new_metasenv_and_unify_and_t dbd proof goal newmeta' metasenv' context term'
         [g1;g2] ->
           let proof'',goals =
            ProofEngineTypes.apply_tactic
-           (auto_tac ~params:["paramodulation","on"] ~dbd) (proof'',g2)
+           (auto_tac ~params:["caso_strano","on";"paramodulation","on"] ~dbd) (proof'',g2)
           in
            let proof'',goals =
             ProofEngineTypes.apply_tactic