aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/funind/invfun.ml11
-rw-r--r--tactics/tauto.ml4249
-rw-r--r--tactics/tauto.mli0
-rw-r--r--test-suite/bugs/closed/2800.v (renamed from test-suite/bugs/opened/2800.v)2
-rw-r--r--theories/Init/Notations.v1
-rw-r--r--theories/Init/Prelude.v1
-rw-r--r--theories/Init/Tauto.v101
-rw-r--r--theories/Init/vo.itarget3
-rw-r--r--theories/Logic/Decidable.v2
9 files changed, 156 insertions, 214 deletions
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index cdb9c5067..6a5a5ad53 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -474,6 +474,15 @@ let generalize_dependent_of x hyp g =
(* [intros_with_rewrite] do the intros in each branch and treat each new hypothesis
(unfolding, substituting, destructing cases \ldots)
*)
+let tauto =
+ let dp = List.map Id.of_string ["Tauto" ; "Init"; "Coq"] in
+ let mp = ModPath.MPfile (DirPath.make dp) in
+ let kn = KerName.make2 mp (Label.make "tauto") in
+ Proofview.tclBIND (Proofview.tclUNIT ()) begin fun () ->
+ let body = Tacenv.interp_ltac kn in
+ Tacinterp.eval_tactic body
+ end
+
let rec intros_with_rewrite g =
observe_tac "intros_with_rewrite" intros_with_rewrite_aux g
and intros_with_rewrite_aux : tactic =
@@ -530,7 +539,7 @@ and intros_with_rewrite_aux : tactic =
] g
end
| Ind _ when eq_constr t (Coqlib.build_coq_False ()) ->
- Proofview.V82.of_tactic Tauto.tauto g
+ Proofview.V82.of_tactic tauto g
| Case(_,_,v,_) ->
tclTHENSEQ[
Proofview.V82.of_tactic (simplest_case v);
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 5485f344b..e0427ae89 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -14,6 +14,7 @@ open Names
open Pp
open Genarg
open Stdarg
+open Misctypes
open Tacexpr
open Tacinterp
open Tactics
@@ -90,6 +91,7 @@ let _ =
(** Base tactics *)
+let loc = Loc.ghost
let idtac = Proofview.tclUNIT ()
let fail = Proofview.tclINDEPENDENT (tclFAIL 0 (Pp.mt ()))
@@ -112,38 +114,9 @@ let split = Tactics.split_with_bindings false [Misctypes.NoBindings]
(** Test *)
-let make_lfun l =
- let fold accu (id, v) = Id.Map.add (Id.of_string id) v accu in
- List.fold_left fold Id.Map.empty l
-
-let register_tauto_tactic tac name =
- let name = { mltac_plugin = "tauto"; mltac_tactic = name; } in
- let entry = { mltac_name = name; mltac_index = 0 } in
- Tacenv.register_ml_tactic name [| tac |];
- TacML (Loc.ghost, entry, [])
-
-let tacticIn_ist tac name =
- let tac _ ist =
- let avoid = Option.default [] (TacStore.get ist.extra f_avoid_ids) in
- let debug = Option.default Tactic_debug.DebugOff (TacStore.get ist.extra f_debug) in
- let (tac, ist) = tac ist in
- interp_tac_gen ist.lfun avoid debug tac
- in
- register_tauto_tactic tac name
-
-let tacticIn tac name =
- tacticIn_ist (fun ist -> tac ist, ist) name
-
-let push_ist ist args =
- let fold accu (id, arg) = Id.Map.add (Id.of_string id) arg accu in
- let lfun = List.fold_left fold ist.lfun args in
- { ist with lfun = lfun }
-
let is_empty _ ist =
if is_empty_type (assoc_var "X1" ist) then idtac else fail
-let t_is_empty = register_tauto_tactic is_empty "is_empty"
-
(* Strictly speaking, this exceeds the propositional fragment as it
matches also equality types (and solves them if a reflexivity) *)
let is_unit_or_eq _ ist =
@@ -151,16 +124,6 @@ let is_unit_or_eq _ ist =
let test = if flags.strict_unit then is_unit_type else is_unit_or_eq_type in
if test (assoc_var "X1" ist) then idtac else fail
-let t_is_unit_or_eq = register_tauto_tactic is_unit_or_eq "is_unit_or_eq"
-
-let is_record t =
- let (hdapp,args) = decompose_app t in
- match (kind_of_term hdapp) with
- | Ind (ind,u) ->
- let (mib,mip) = Global.lookup_inductive ind in
- mib.Declarations.mind_record <> None
- | _ -> false
-
let bugged_is_binary t =
isApp t &&
let (hdapp,args) = decompose_app t in
@@ -182,8 +145,6 @@ let is_conj _ ist =
then idtac
else fail
-let t_is_conj = register_tauto_tactic is_conj "is_conj"
-
let flatten_contravariant_conj _ ist =
let flags = assoc_flags ist in
let typ = assoc_var "X1" ist in
@@ -200,18 +161,8 @@ let flatten_contravariant_conj _ ist =
tclTHENLIST [assert_ ~by newtyp; clear (destVar hyp)]
| _ -> fail
-let t_flatten_contravariant_conj =
- register_tauto_tactic flatten_contravariant_conj "flatten_contravariant_conj"
-
(** Dealing with disjunction *)
-let constructor i =
- let name = { Tacexpr.mltac_plugin = "coretactics"; mltac_tactic = "constructor" } in
- (** Take care of the index: this is the second entry in constructor. *)
- let name = { Tacexpr.mltac_name = name; mltac_index = 1 } in
- let i = in_gen (rawwit Constrarg.wit_int_or_var) (Misctypes.ArgArg i) in
- Tacexpr.TacML (Loc.ghost, name, [TacGeneric i])
-
let is_disj _ ist =
let flags = assoc_flags ist in
let t = assoc_var "X1" ist in
@@ -222,8 +173,6 @@ let is_disj _ ist =
then idtac
else fail
-let t_is_disj = register_tauto_tactic is_disj "is_disj"
-
let flatten_contravariant_disj _ ist =
let flags = assoc_flags ist in
let typ = assoc_var "X1" ist in
@@ -245,159 +194,30 @@ let flatten_contravariant_disj _ ist =
tclTHEN (tclTHENLIST tacs) tac0
| _ -> fail
-let t_flatten_contravariant_disj =
- register_tauto_tactic flatten_contravariant_disj "flatten_contravariant_disj"
-
-(** Main tactic *)
-
-let not_dep_intros ist =
- <:tactic<
- repeat match goal with
- | |- (forall (_: ?X1), ?X2) => intro
- | |- (Coq.Init.Logic.not _) => unfold Coq.Init.Logic.not at 1; intro
- end >>
-
-let t_not_dep_intros = tacticIn not_dep_intros "not_dep_intros"
-
-let axioms ist =
- let c1 = constructor 1 in
- <:tactic<
- match reverse goal with
- | |- ?X1 => $t_is_unit_or_eq; $c1
- | _:?X1 |- _ => $t_is_empty; elimtype X1; assumption
- | _:?X1 |- ?X1 => assumption
- end >>
-
-let t_axioms = tacticIn axioms "axioms"
-
-let simplif ist =
- let c1 = constructor 1 in
- <:tactic<
- $t_not_dep_intros;
- repeat
- (match reverse goal with
- | id: ?X1 |- _ => $t_is_conj; elim id; do 2 intro; clear id
- | id: (Coq.Init.Logic.iff _ _) |- _ => elim id; do 2 intro; clear id
- | id: (Coq.Init.Logic.not _) |- _ => red in id
- | id: ?X1 |- _ => $t_is_disj; elim id; intro; clear id
- | id0: (forall (_: ?X1), ?X2), id1: ?X1|- _ =>
- (* generalize (id0 id1); intro; clear id0 does not work
- (see Marco Maggiesi's bug PR#301)
- so we instead use Assert and exact. *)
- assert X2; [exact (id0 id1) | clear id0]
- | id: forall (_ : ?X1), ?X2|- _ =>
- $t_is_unit_or_eq; cut X2;
- [ intro; clear id
- | (* id : forall (_: ?X1), ?X2 |- ?X2 *)
- cut X1; [exact id| $c1; fail]
- ]
- | id: forall (_ : ?X1), ?X2|- _ =>
- $t_flatten_contravariant_conj
- (* moved from "id:(?A/\?B)->?X2|-" to "?A->?B->?X2|-" *)
- | id: forall (_: Coq.Init.Logic.iff ?X1 ?X2), ?X3|- _ =>
- assert (forall (_: forall _:X1, X2), forall (_: forall _: X2, X1), X3)
- by (do 2 intro; apply id; split; assumption);
- clear id
- | id: forall (_:?X1), ?X2|- _ =>
- $t_flatten_contravariant_disj
- (* moved from "id:(?A\/?B)->?X2|-" to "?A->?X2,?B->?X2|-" *)
- | |- ?X1 => $t_is_conj; split
- | |- (Coq.Init.Logic.iff _ _) => split
- | |- (Coq.Init.Logic.not _) => red
- end;
- $t_not_dep_intros) >>
-
-let t_simplif = tacticIn simplif "simplif"
-
-let tauto_intuit flags t_reduce solver =
- let flags = Genarg.Val.Dyn (Genarg.val_tag (topwit wit_tauto_flags), flags) in
- let lfun = make_lfun [("t_solver", solver); ("tauto_flags", flags)] in
- let ist = { default_ist () with lfun = lfun; } in
- let vars = [Id.of_string "t_solver"] in
- (vars, ist, <:tactic<
- let rec t_tauto_intuit :=
- ($t_simplif;$t_axioms
- || match reverse goal with
- | id:forall(_: forall (_: ?X1), ?X2), ?X3|- _ =>
- cut X3;
- [ intro; clear id; t_tauto_intuit
- | cut (forall (_: X1), X2);
- [ exact id
- | generalize (fun y:X2 => id (fun x:X1 => y)); intro; clear id;
- solve [ t_tauto_intuit ]]]
- | id:forall (_:not ?X1), ?X3|- _ =>
- cut X3;
- [ intro; clear id; t_tauto_intuit
- | cut (not X1); [ exact id | clear id; intro; solve [t_tauto_intuit ]]]
- | |- ?X1 =>
- $t_is_disj; solve [left;t_tauto_intuit | right;t_tauto_intuit]
- end
- ||
- (* NB: [|- _ -> _] matches any product *)
- match goal with | |- forall (_ : _), _ => intro; t_tauto_intuit
- | |- _ => $t_reduce;t_solver
- end
- ||
- t_solver
- ) in t_tauto_intuit >>)
-
-let reduction_not_iff _ist =
- match !negation_unfolding, unfold_iff () with
+let reduction_not_iff _ ist =
+ let avoid = Option.default [] (TacStore.get ist.extra f_avoid_ids) in
+ let debug = Option.default Tactic_debug.DebugOff (TacStore.get ist.extra f_debug) in
+ let tac = match !negation_unfolding, unfold_iff () with
| true, true -> <:tactic< unfold Coq.Init.Logic.not, Coq.Init.Logic.iff in * >>
| true, false -> <:tactic< unfold Coq.Init.Logic.not in * >>
| false, true -> <:tactic< unfold Coq.Init.Logic.iff in * >>
| false, false -> <:tactic< idtac >>
-
-let t_reduction_not_iff = tacticIn reduction_not_iff "reduction_not_iff"
-
-let intuition_gen ist flags tac =
- Proofview.Goal.enter { enter = begin fun gl ->
- let env = Proofview.Goal.env gl in
- let vars, ist, intuition = tauto_intuit flags t_reduction_not_iff tac in
- let glb_intuition = Tacintern.glob_tactic_env vars env intuition in
- eval_tactic_ist ist glb_intuition
- end }
-
-let tauto_intuitionistic flags =
- let fail = Value.of_closure (default_ist ()) <:tactic<fail>> in
- Proofview.tclORELSE
- (intuition_gen (default_ist ()) flags fail)
- begin function (e, info) -> match e with
- | Refiner.FailError _ | UserError _ ->
- Tacticals.New.tclZEROMSG (str "tauto failed.")
- | e -> Proofview.tclZERO ~info e
- end
+ in
+ interp_tac_gen ist.lfun avoid debug tac
let coq_nnpp_path =
let dir = List.map Id.of_string ["Classical_Prop";"Logic";"Coq"] in
Libnames.make_path (DirPath.make dir) (Id.of_string "NNPP")
-let tauto_classical flags nnpp =
- Proofview.tclORELSE
- (Tacticals.New.tclTHEN (apply nnpp) (tauto_intuitionistic flags))
- begin function (e, info) -> match e with
- | UserError _ -> Tacticals.New.tclZEROMSG (str "Classical tauto failed.")
- | e -> Proofview.tclZERO ~info e
- end
-
-let tauto_gen flags =
- (* spiwack: I use [tclBIND (tclUNIT ())] as a way to delay the effect
- (in [constr_of_global]) to the application of the tactic. *)
+let apply_nnpp _ ist =
Proofview.tclBIND
(Proofview.tclUNIT ())
begin fun () -> try
let nnpp = Universes.constr_of_global (Nametab.global_of_path coq_nnpp_path) in
- (* try intuitionistic version first to avoid an axiom if possible *)
- Tacticals.New.tclORELSE (tauto_intuitionistic flags) (tauto_classical flags nnpp)
- with Not_found ->
- tauto_intuitionistic flags
+ apply nnpp
+ with Not_found -> tclFAIL 0 (Pp.mt ())
end
-let default_intuition_tac =
- let tac _ _ = Auto.h_auto None [] None in
- let tac = register_tauto_tactic tac "auto_with" in
- Value.of_closure (default_ist ()) tac
-
(* This is the uniform mode dealing with ->, not, iff and types isomorphic to
/\ and *, \/ and +, False and Empty_set, True and unit, _and_ eq-like types.
For the moment not and iff are still always unfolded. *)
@@ -427,23 +247,34 @@ let tauto_power_flags = {
strict_unit = false
}
-let tauto = tauto_gen tauto_uniform_unit_flags
-let dtauto = tauto_gen tauto_power_flags
-
-TACTIC EXTEND tauto
-| [ "tauto" ] -> [ tauto ]
-END
-
-TACTIC EXTEND dtauto
-| [ "dtauto" ] -> [ dtauto ]
+let with_flags flags ist tac =
+ let f = (loc, Id.of_string "f") in
+ let x = (loc, Id.of_string "x") in
+ let arg = Val.Dyn (val_tag (topwit wit_tauto_flags), flags) in
+ let ist = { ist with lfun = Id.Map.add (snd f) tac (Id.Map.add (snd x) arg ist.lfun) } in
+ eval_tactic_ist ist (TacArg (loc, TacCall (loc, ArgVar f, [Reference (ArgVar x)])))
+
+TACTIC EXTEND with_flags
+| [ "with_uniform_flags" tactic(tac) ] -> [ with_flags tauto_uniform_unit_flags ist tac ]
+| [ "with_legacy_flags" tactic(tac) ] -> [ with_flags tauto_legacy_flags ist tac ]
+| [ "with_power_flags" tactic(tac) ] -> [ with_flags tauto_power_flags ist tac ]
END
-TACTIC EXTEND intuition
-| [ "intuition" ] -> [ intuition_gen ist tauto_uniform_unit_flags default_intuition_tac ]
-| [ "intuition" tactic(t) ] -> [ intuition_gen ist tauto_uniform_unit_flags t ]
-END
-
-TACTIC EXTEND dintuition
-| [ "dintuition" ] -> [ intuition_gen ist tauto_power_flags default_intuition_tac ]
-| [ "dintuition" tactic(t) ] -> [ intuition_gen ist tauto_power_flags t ]
-END
+let register_tauto_tactic_ tac name0 args =
+ let ids = List.map (fun id -> Id.of_string id) args in
+ let ids = List.map (fun id -> Some id) ids in
+ let name = { mltac_plugin = "tauto"; mltac_tactic = name0 ^ "_"; } in
+ let entry = { mltac_name = name; mltac_index = 0 } in
+ let () = Tacenv.register_ml_tactic name [| tac |] in
+ let tac = TacFun (ids, TacML (loc, entry, [])) in
+ let obj () = Tacenv.register_ltac true true (Id.of_string name0) tac in
+ Mltop.declare_cache_obj obj "tauto"
+
+let () = register_tauto_tactic_ is_empty "is_empty" ["tauto_flags"; "X1"]
+let () = register_tauto_tactic_ is_unit_or_eq "is_unit_or_eq" ["tauto_flags"; "X1"]
+let () = register_tauto_tactic_ is_disj "is_disj" ["tauto_flags"; "X1"]
+let () = register_tauto_tactic_ is_conj "is_conj" ["tauto_flags"; "X1"]
+let () = register_tauto_tactic_ flatten_contravariant_disj "flatten_contravariant_disj" ["tauto_flags"; "X1"; "X2"; "id"]
+let () = register_tauto_tactic_ flatten_contravariant_conj "flatten_contravariant_conj" ["tauto_flags"; "X1"; "X2"; "id"]
+let () = register_tauto_tactic_ apply_nnpp "apply_nnpp" []
+let () = register_tauto_tactic_ reduction_not_iff "reduction_not_iff" []
diff --git a/tactics/tauto.mli b/tactics/tauto.mli
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/tactics/tauto.mli
diff --git a/test-suite/bugs/opened/2800.v b/test-suite/bugs/closed/2800.v
index c559ab0c1..2ee438934 100644
--- a/test-suite/bugs/opened/2800.v
+++ b/test-suite/bugs/closed/2800.v
@@ -1,6 +1,6 @@
Goal False.
-Fail intuition
+intuition
match goal with
| |- _ => idtac " foo"
end.
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index e1ddaeaef..55eb699be 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -90,4 +90,3 @@ Declare ML Module "eauto".
Declare ML Module "g_class".
Declare ML Module "g_eqdecide".
Declare ML Module "g_rewrite".
-Declare ML Module "tauto".
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index 04a263ad9..03f2328de 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -15,6 +15,7 @@ Require Coq.Init.Nat.
Require Export Peano.
Require Export Coq.Init.Wf.
Require Export Coq.Init.Tactics.
+Require Export Coq.Init.Tauto.
(* Initially available plugins
(+ nat_syntax_plugin loaded in Datatypes) *)
Declare ML Module "extraction_plugin".
diff --git a/theories/Init/Tauto.v b/theories/Init/Tauto.v
new file mode 100644
index 000000000..e0949eb73
--- /dev/null
+++ b/theories/Init/Tauto.v
@@ -0,0 +1,101 @@
+Require Import Notations.
+Require Import Datatypes.
+Require Import Logic.
+
+Local Declare ML Module "tauto".
+
+Local Ltac not_dep_intros :=
+ repeat match goal with
+ | |- (forall (_: ?X1), ?X2) => intro
+ | |- (Coq.Init.Logic.not _) => unfold Coq.Init.Logic.not at 1; intro
+ end.
+
+Local Ltac axioms flags :=
+ match reverse goal with
+ | |- ?X1 => is_unit_or_eq flags X1; constructor 1
+ | _:?X1 |- _ => is_empty flags X1; elimtype X1; assumption
+ | _:?X1 |- ?X1 => assumption
+ end.
+
+Local Ltac simplif flags :=
+ not_dep_intros;
+ repeat
+ (match reverse goal with
+ | id: ?X1 |- _ => is_conj flags X1; elim id; do 2 intro; clear id
+ | id: (Coq.Init.Logic.iff _ _) |- _ => elim id; do 2 intro; clear id
+ | id: (Coq.Init.Logic.not _) |- _ => red in id
+ | id: ?X1 |- _ => is_disj flags X1; elim id; intro; clear id
+ | id0: (forall (_: ?X1), ?X2), id1: ?X1|- _ =>
+ (* generalize (id0 id1); intro; clear id0 does not work
+ (see Marco Maggiesi's bug PR#301)
+ so we instead use Assert and exact. *)
+ assert X2; [exact (id0 id1) | clear id0]
+ | id: forall (_ : ?X1), ?X2|- _ =>
+ is_unit_or_eq flags X1; cut X2;
+ [ intro; clear id
+ | (* id : forall (_: ?X1), ?X2 |- ?X2 *)
+ cut X1; [exact id| constructor 1; fail]
+ ]
+ | id: forall (_ : ?X1), ?X2|- _ =>
+ flatten_contravariant_conj flags X1 X2 id
+ (* moved from "id:(?A/\?B)->?X2|-" to "?A->?B->?X2|-" *)
+ | id: forall (_: Coq.Init.Logic.iff ?X1 ?X2), ?X3|- _ =>
+ assert (forall (_: forall _:X1, X2), forall (_: forall _: X2, X1), X3)
+ by (do 2 intro; apply id; split; assumption);
+ clear id
+ | id: forall (_:?X1), ?X2|- _ =>
+ flatten_contravariant_disj flags X1 X2 id
+ (* moved from "id:(?A\/?B)->?X2|-" to "?A->?X2,?B->?X2|-" *)
+ | |- ?X1 => is_conj flags X1; split
+ | |- (Coq.Init.Logic.iff _ _) => split
+ | |- (Coq.Init.Logic.not _) => red
+ end;
+ not_dep_intros).
+
+Local Ltac tauto_intuit flags t_reduce t_solver :=
+ let rec t_tauto_intuit :=
+ (simplif flags; axioms flags
+ || match reverse goal with
+ | id:forall(_: forall (_: ?X1), ?X2), ?X3|- _ =>
+ cut X3;
+ [ intro; clear id; t_tauto_intuit
+ | cut (forall (_: X1), X2);
+ [ exact id
+ | generalize (fun y:X2 => id (fun x:X1 => y)); intro; clear id;
+ solve [ t_tauto_intuit ]]]
+ | id:forall (_:not ?X1), ?X3|- _ =>
+ cut X3;
+ [ intro; clear id; t_tauto_intuit
+ | cut (not X1); [ exact id | clear id; intro; solve [t_tauto_intuit ]]]
+ | |- ?X1 =>
+ is_disj flags X1; solve [left;t_tauto_intuit | right;t_tauto_intuit]
+ end
+ ||
+ (* NB: [|- _ -> _] matches any product *)
+ match goal with | |- forall (_ : _), _ => intro; t_tauto_intuit
+ | |- _ => t_reduce;t_solver
+ end
+ ||
+ t_solver
+ ) in t_tauto_intuit.
+
+Local Ltac intuition_gen flags solver := tauto_intuit flags reduction_not_iff solver.
+Local Ltac tauto_intuitionistic flags := intuition_gen flags fail || fail "tauto failed".
+Local Ltac tauto_classical flags :=
+ (apply_nnpp || fail "tauto failed"); (tauto_intuitionistic flags || fail "Classical tauto failed").
+Local Ltac tauto_gen flags := tauto_intuitionistic flags || tauto_classical flags.
+
+Ltac tauto := with_uniform_flags (fun flags => tauto_gen flags).
+Ltac dtauto := with_power_flags (fun flags => tauto_gen flags).
+
+Ltac intuition := with_uniform_flags (fun flags => intuition_gen flags ltac:(auto with *)).
+Local Ltac intuition_then tac := with_uniform_flags (fun flags => intuition_gen flags tac).
+
+Ltac dintuition := with_power_flags (fun flags => intuition_gen flags ltac:(auto with *)).
+Local Ltac dintuition_then tac := with_power_flags (fun flags => intuition_gen flags tac).
+
+Tactic Notation "intuition" := intuition.
+Tactic Notation "intuition" tactic(t) := intuition_then t.
+
+Tactic Notation "dintuition" := dintuition.
+Tactic Notation "dintuition" tactic(t) := dintuition_then t.
diff --git a/theories/Init/vo.itarget b/theories/Init/vo.itarget
index cc62e66cc..99877065e 100644
--- a/theories/Init/vo.itarget
+++ b/theories/Init/vo.itarget
@@ -7,4 +7,5 @@ Prelude.vo
Specif.vo
Tactics.vo
Wf.vo
-Nat.vo \ No newline at end of file
+Nat.vo
+Tauto.vo
diff --git a/theories/Logic/Decidable.v b/theories/Logic/Decidable.v
index 2ba7253c4..8b6054f9d 100644
--- a/theories/Logic/Decidable.v
+++ b/theories/Logic/Decidable.v
@@ -50,7 +50,7 @@ Qed.
Theorem dec_iff :
forall A B:Prop, decidable A -> decidable B -> decidable (A<->B).
Proof.
-unfold decidable; tauto.
+unfold decidable. tauto.
Qed.
Theorem not_not : forall P:Prop, decidable P -> ~ ~ P -> P.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-07 03:31:49 +0000