From bdcc72576adf78333d0e4035b42c4ea26583b921 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 2 May 2000 13:05:21 +0000
Subject: Problème avec motif du second-ordre

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@395 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tauto.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/tactics/tauto.ml b/tactics/tauto.ml
index 7010aba19f..2708bf01ae 100644
--- a/tactics/tauto.ml
+++ b/tactics/tauto.ml
@@ -53,14 +53,17 @@ let true_pattern_mark = put_pat mmk "True"
 let and_pattern_mark   = put_pat mmk "(and ?1 ?2)"
 let or_pattern_mark    = put_pat mmk "(or ?1 ?2)"
 let eq_pattern_mark    = put_pat mmk "(eq ?1 ?2 ?3)"
-let pi_pattern    = put_pat mmk "(x : ?)((?)@[x])"
+let pi_pattern    = put_pat mmk "(x : ?)((?1)@[x])"
 let imply_pattern = put_pat mmk "?1 -> ?2"
 let atomic_imply_bot_pattern = put_pat mmk "?1 -> ?2"
 let iff_pattern_mark   = put_pat mmk "(iff ?1 ?2)"
 let not_pattern_mark   = put_pat mmk "(not ?1)"
 (* squeletons *)
+(*
 let imply_squeleton = put_squel mmk "?1 -> ?2"
-let mkIMP a b       = soinstance imply_squeleton [a;b]    
+let mkIMP a b = soinstance imply_squeleton [a;b]
+*)
+let mkIMP a b = mkProd Anonymous a b
 
 let false_pattern () = get_pat false_pattern_mark
 let true_pattern () = get_pat true_pattern_mark
-- 
cgit v1.2.3