last cleanup

classical/contra.v

@@ -1,4 +1,4 @@
-(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
+(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
 Require Import boolp.
@@ -66,7 +66,6 @@ Notation "\Forall x .. z , T" :=
   (at level 200, x binder, z binder, T at level 200,
    format "'[hv' '\Forall'  '[' x .. z , ']' '/ '  T ']'") : type_scope.
 
-(* TOTHINK: This mentions a Coq 8.12 issue. Is it still needed? *)
 (*  The ForallI implementation has to work around several Coq 8.12 issues:    *)
 (*    - Coq unification defers Type constraints so we must ensure the type    *)
 (*      constraint for the forall term F is processed, and the resulting      *)
@@ -82,11 +81,11 @@ Notation "\Forall x .. z , T" :=
 (*      equality destruction.                                                 *)
 (*    - ssr case: and set do not recognize ssrpatternarg parameters, so we    *)
 (*      must rely on ssrmatching.ssrpattern.                                  *)
-(* Tactic Notation "ForallI" ssrpatternarg(pat) :=
+Tactic Notation "ForallI" ssrpatternarg(pat) :=
   let F := fresh "F" in ssrmatching.ssrpattern pat => F;
   case: F / (@erefl _ F : Forall _ = _).
 Tactic Notation "ForallI" := ForallI (forall x, _).
- *)
+
 
 (******************************************************************************)
 (*   We define specialized copies of the wrapped structure of ssrfun for Prop *)
@@ -724,7 +723,6 @@ Tactic Notation "contra" ":" "{" "-" "}" constr(H) := contra: (H).
 (* The ':' form absurd: <d-items> replaces the goal with the negation of the  *)
 (* (single) <d-item> (as with contra:, a clear switch is also allowed.        *)
 (* Finally the Ltac absurd term form is also supported.                       *)
-(* TOTHINK: Why not simply use exfalso? *)
 Lemma absurd T : False -> T. Proof. by []. Qed.
 Tactic Notation (at level 0) "absurd" := apply absurd.
 Tactic Notation (at level 0) "absurd" constr(P) := have []: ~ P.