summaryrefslogtreecommitdiff
path: root/tactics/tauto.ml4
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:02:20 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:02:20 +0100
commit97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch)
tree97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /tactics/tauto.ml4
parent300293c119981054c95182a90c829058530a6b6f (diff)
Imported Upstream version 8.4~betaupstream/8.4_beta
Diffstat (limited to 'tactics/tauto.ml4')
-rw-r--r--tactics/tauto.ml413
1 files changed, 6 insertions, 7 deletions
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index a17aba76..b7a58be4 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -8,8 +8,6 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(*i $Id: tauto.ml4 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
open Term
open Hipattern
open Names
@@ -55,6 +53,7 @@ open Goptions
let _ =
declare_bool_option
{ optsync = true;
+ optdepr = false;
optname = "unfolding of iff and not in intuition";
optkey = ["Intuition";"Iff";"Unfolding"];
optread = (fun () -> !iff_unfolding);
@@ -154,10 +153,12 @@ let flatten_contravariant_disj ist =
let hyp = valueIn (VConstr ([],hyp)) in
iter_tac (list_map_i (fun i arg ->
let typ = valueIn (VConstr ([],mkArrow arg c)) in
+ let i = Tacexpr.Integer i in
<:tactic<
let typ := $typ in
let hyp := $hyp in
- assert typ by (intro; apply hyp; constructor $i; assumption)
+ let i := $i in
+ assert typ by (intro; apply hyp; constructor i; assumption)
>>) 1 args) <:tactic< let hyp := $hyp in clear hyp >>
else
<:tactic<fail>>
@@ -268,8 +269,6 @@ let t_reduction_not = tacticIn reduction_not
let intuition_gen tac =
interp (tacticIn (tauto_intuit t_reduction_not tac))
-let simplif_gen = interp (tacticIn simplif)
-
let tauto_intuitionistic g =
try intuition_gen <:tactic<fail>> g
with
@@ -301,5 +300,5 @@ END
TACTIC EXTEND intuition
| [ "intuition" ] -> [ intuition_gen default_intuition_tac ]
-| [ "intuition" tactic(t) ] -> [ intuition_gen (fst t) ]
+| [ "intuition" tactic(t) ] -> [ intuition_gen t ]
END