From a507a21ca97552dec5077667cf8433f24d7a45ae Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Jun 2006 16:54:28 +0000 Subject: [PATCH] using the new metadataConstraint function --- helm/software/components/tactics/autoTactic.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/helm/software/components/tactics/autoTactic.ml b/helm/software/components/tactics/autoTactic.ml index 63dc8631d..d4dc5592c 100644 --- a/helm/software/components/tactics/autoTactic.ml +++ b/helm/software/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 -- 2.39.2