From 2e233fd5358ca0ee124114563a8414e49f336b13 Mon Sep 17 00:00:00 2001 From: barras Date: Thu, 13 Nov 2003 15:49:27 +0000 Subject: factorisation et generalisation des clauses git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4892 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/interface/blast.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'contrib/interface/blast.ml') diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml index 7d3ed8dd8..a7e98b69d 100755 --- a/contrib/interface/blast.ml +++ b/contrib/interface/blast.ml @@ -516,7 +516,7 @@ let blast_auto = (free_try default_full_auto) (free_try (my_full_eauto 2))) *) ;; -let blast_simpl = (free_try (reduce (Simpl None) [])) +let blast_simpl = (free_try (reduce (Simpl None) onConcl)) ;; let blast_induction1 = (free_try (tclTHEN (tclTRY intro) -- cgit v1.2.3