Introduction d'un type constr_pattern pour les différents filtrages

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@368 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 5 insertions, 2 deletions

diff --git a/tactics/tauto.ml b/tactics/tauto.ml
index 4fcfc0264..334eb304e 100644
--- a/tactics/tauto.ml
+++ b/tactics/tauto.ml
@@ -46,6 +46,7 @@ let classically cltac = function
 
 let somatch m pat = somatch None (get_pat pat) m
 let module_mark   = ["Logic"]
+(* patterns *)
 let mmk           = make_module_marker ["Prelude"]
 let false_pattern = put_pat mmk "False"
 let true_pattern = put_pat mmk "True"
@@ -54,9 +55,12 @@ let or_pattern    = put_pat mmk "(or ? ?)"
 let eq_pattern    = put_pat mmk "(eq ? ? ?)"
 let pi_pattern    = put_pat mmk "(x : ?)((?)@[x])"
 let imply_pattern = put_pat mmk "?1 -> ?2"
+let atomic_imply_bot_pattern = put_pat mmk "?1 -> ?2"
 let iff_pattern   = put_pat mmk "(iff ? ?)"
 let not_pattern   = put_pat mmk "(not ?1)"
-let mkIMP a b     = soinstance imply_pattern [a;b]    
+(* squeletons *)
+let imply_squeleton = put_pat mmk "?1 -> ?2"
+let mkIMP a b       = soinstance imply_squeleton [a;b]    
 
 let is_atomic m =
  (not (is_conjunction m)     ||
@@ -120,7 +124,6 @@ let dyck_imply_intro = (dImp None)
     --------------
     A->B,A,Gamma |- G  (A Atomique)
  *)
-let atomic_imply_bot_pattern = put_pat mmk "?1 -> ?2"
 
 let atomic_imply_step cls gls =
   let mvb = somatch (clause_type cls gls) atomic_imply_bot_pattern in