From: Enrico Tassi 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