Farewell decl_mode

This commit removes from the source tree plugins/decl_mode,
its chapter in the reference manual and related tests.

5 files changed, 0 insertions, 585 deletions

diff --git a/test-suite/bugs/closed/2640.v b/test-suite/bugs/closed/2640.v
deleted file mode 100644
index da0cc68a4..000000000
--- a/test-suite/bugs/closed/2640.v
+++ /dev/null
@@ -1,17 +0,0 @@
-(* Testing consistency of globalization and interpretation in some
-   extreme cases *)
-
-Section sect.
-
-  (* Simplification of the initial example *)
-  Hypothesis Other: True.
-
-  Lemma C2 : True.
-  proof.
-  Fail have True using Other.
-  Abort.
-
-  (* Variant of the same problem *)
-  Lemma C2 : True.
-  Fail clear; Other.
-  Abort.
diff --git a/test-suite/ide/undo.v b/test-suite/ide/undo.v
deleted file mode 100644
index ea3920551..000000000
--- a/test-suite/ide/undo.v
+++ /dev/null
@@ -1,103 +0,0 @@
-(* Here are a sequences of scripts to test interactively with undo and
-   replay in coqide proof sessions *)
-
-(* Undoing arbitrary commands, as first step *)
-
-Theorem a : O=O. (* 2 *)
-Ltac f x := x. (* 1 * 3 *)
-assert True by trivial.
-trivial.
-Qed.
-
-(* Undoing arbitrary commands, as non-first step *)
-
-Theorem b : O=O.
-assert True by trivial.
-Ltac g x := x.
-assert True by trivial.
-trivial.
-Qed.
-
-(* Undoing declarations, as first step *)
-(* was bugged in 8.1 *)
-
-Theorem c : O=O.
-Inductive T : Type := I.
-trivial.
-Qed.
-
-(* Undoing declarations, as first step *)
-(* new in 8.2 *)
-
-Theorem d : O=O.
-Definition e := O.
-Definition f := O.
-assert True by trivial.
-trivial.
-Qed.
-
-(* Undoing declarations, as non-first step *)
-(* new in 8.2 *)
-
-Theorem h : O=O.
-assert True by trivial.
-Definition i := O.
-Definition j := O.
-assert True by trivial.
-trivial.
-Qed.
-
-(* Undoing declarations, interleaved with proof steps *)
-(* new in 8.2 *)
-
-Theorem k : O=O.
-assert True by trivial.
-Definition l := O.
-assert True by trivial.
-Definition m := O.
-assert True by trivial.
-trivial.
-Qed.
-
-(* Undoing declarations, interleaved with proof steps and commands *)
-(* new in 8.2 *)
-
-Theorem n : O=O.
-assert True by trivial.
-Definition o := O.
-Ltac h x := x.
-assert True by trivial.
-Focus.
-Definition p := O.
-assert True by trivial.
-trivial.
-Qed.
-
-(* Undoing declarations, not in proof *)
-
-Definition q := O.
-Definition r := O.
-
-(* Bug 2082 : Follow the numbers *)
-(* Broken due to proof engine rewriting *)
-
-Variable A : Prop.
-Variable B : Prop.
-
-Axiom OR : A \/ B.
-
-Lemma MyLemma2 : True.
-proof.
-per cases of (A \/ B) by OR.
-suppose A.
-    then (1 = 1).
-    then H1 : thesis. (* 4 *)
-    thus thesis by H1. (* 2 *)
-suppose B. (* 1 *) (* 3 *)
-    then (1 = 1).
-    then H2 : thesis.
-    thus thesis by H2.
-end cases.
-end proof.
-Qed. (* 5 if you made it here, there is no regression *)
-
diff --git a/test-suite/ide/undo011.fake b/test-suite/ide/undo011.fake
deleted file mode 100644
index 0be439b27..000000000
--- a/test-suite/ide/undo011.fake
+++ /dev/null
@@ -1,34 +0,0 @@
-# Script simulating a dialog between coqide and coqtop -ideslave
-# Run it via fake_ide
-#
-# Bug 2082
-# Broken due to proof engine rewriting
-#
-ADD { Variable A : Prop. }
-ADD { Variable B : Prop. }
-ADD { Axiom OR : A \/ B. }
-ADD { Lemma MyLemma2 : True. }
-ADD { proof. }
-ADD { per cases of (A \/ B) by OR. }
-ADD { suppose A. }
-ADD {     then (1 = 1). }
-ADD there {     then H1 : thesis. }
-ADD here {     thus thesis by H1. }
-ADD { suppose B. }
-QUERY { Show. }
-EDIT_AT here
-# <replay>
-ADD { suppose B. }
-# </replay>
-EDIT_AT there
-# <replay>
-ADD {    thus thesis by H1. }
-ADD { suppose B. }
-# </replay>
-QUERY { Show. }
-ADD {    then (1 = 1). }
-ADD {    then H2 : thesis. }
-ADD {    thus thesis by H2. }
-ADD { end cases. } 
-ADD { end proof. }
-ADD { Qed. }
diff --git a/test-suite/success/decl_mode.v b/test-suite/success/decl_mode.v
deleted file mode 100644
index 58f79d45e..000000000
--- a/test-suite/success/decl_mode.v
+++ /dev/null
@@ -1,182 +0,0 @@
-(* \sqrt 2 is irrationnal, (c) 2006 Pierre Corbineau *)
-
-Set Firstorder Depth 1.
-Require Import ArithRing Wf_nat Peano_dec Div2 Even Lt.
-
-Lemma double_div2: forall n, div2 (double n) = n.
-proof.
-  assume n:nat.
-  per induction on n.
-    suppose it is 0.
-     suffices (0=0) to show thesis.
-     thus thesis.
-    suppose it is (S m) and Hrec:thesis for m.
-      have (div2 (double (S m))= div2 (S (S (double m)))).
-           ~= (S (div2 (double m))).
-      thus ~= (S m) by Hrec.
-  end induction.
-end proof.
-Show Script.
-Qed.
-
-Lemma double_inv : forall n m, double n = double m -> n = m .
-proof.
-  let n, m be such that H:(double n = double m).
-have (n = div2 (double n)) by double_div2,H.
-       ~= (div2 (double m)) by H.
-  thus ~= m by double_div2.
-end proof.
-Qed.
-
-Lemma double_mult_l : forall n m, (double (n * m)=n * double m).
-proof.
-  assume n:nat and m:nat.
-  have (double (n * m) = n*m + n * m).
-       ~= (n * (m+m)) by * using ring.
-  thus ~= (n * double m).
-end proof.
-Qed.
-
-Lemma double_mult_r : forall n m, (double (n * m)=double n * m).
-proof.
-  assume n:nat and m:nat.
-  have (double (n * m) = n*m + n * m).
-       ~= ((n + n) * m) by * using ring.
-  thus ~= (double n * m).
-end proof.
-Qed.
-
-Lemma even_is_even_times_even: forall n, even (n*n) -> even n.
-proof.
-  let n be such that H:(even (n*n)).
-  per cases of (even n \/ odd n) by even_or_odd.
-    suppose (odd n).
-      hence thesis by H,even_mult_inv_r.
-  end cases.
-end proof.
-Qed.
-
-Lemma main_thm_aux: forall n,even n ->
-double (double (div2 n *div2 n))=n*n.
-proof.
-  given n such that H:(even n).
- *** have (double (double (div2 n * div2 n))
-        = double (div2 n) * double (div2 n))
-        by double_mult_l,double_mult_r.
-  thus ~= (n*n) by H,even_double.
-end proof.
-Qed.
-
-Require Import Omega.
-
-Lemma even_double_n: (forall m, even (double m)).
-proof.
-  assume m:nat.
-  per induction on m.
-    suppose it is 0.
-      thus thesis.
-    suppose it is (S mm) and thesis for mm.
-      then H:(even (S (S (mm+mm)))).
-      have (S (S (mm + mm)) = S mm + S mm)  using omega.
-      hence (even (S mm +S mm)) by H.
-  end induction.
-end proof.
-Qed.
-
-Theorem main_theorem: forall n p, n*n=double (p*p) -> p=0.
-proof.
-  assume n0:nat.
-  define P n as (forall p, n*n=double (p*p) -> p=0).
-  claim rec_step: (forall n, (forall m,m<n-> P m) -> P n).
-    let n be such that H:(forall m : nat, m < n -> P m) and p:nat .
-    per cases of ({n=0}+{n<>0}) by eq_nat_dec.
-      suppose H1:(n=0).
-        per cases on p.
-          suppose it is (S p').
-            assume (n * n = double (S p' * S p')).
-              =~ 0 by H1,mult_n_O.
-              ~= (S (  p' + p' * S p' + S p'* S p'))
-                by plus_n_Sm.
-            hence thesis .
-          suppose it is 0.
-            thus thesis.
-        end cases.
-      suppose H1:(n<>0).
-        assume H0:(n*n=double (p*p)).
-        have (even (double (p*p))) by even_double_n .
-        then (even (n*n)) by H0.
-        then H2:(even n) by even_is_even_times_even.
-        then (double (double (div2 n *div2 n))=n*n)
-          by main_thm_aux.
-          ~= (double (p*p)) by H0.
-        then H':(double (div2 n *div2 n)= p*p) by double_inv.
-        have (even (double (div2 n *div2 n))) by even_double_n.
-        then (even (p*p)) by even_double_n,H'.
-        then H3:(even p) by even_is_even_times_even.
-        have (double(double (div2 n * div2 n)) = n*n)
-          by H2,main_thm_aux.
-          ~= (double (p*p)) by H0.
-          ~= (double(double (double (div2 p * div2 p))))
-            by H3,main_thm_aux.
-        then H'':(div2 n * div2 n = double (div2 p * div2 p))
-          by double_inv.
-        then (div2 n < n) by lt_div2,neq_O_lt,H1.
-        then H4:(div2 p=0) by  (H (div2 n)),H''.
-        then (double (div2 p) = double 0).
-             =~ p by even_double,H3.
-        thus ~= 0.
-    end cases.
-  end claim.
-  hence thesis by (lt_wf_ind n0 P).
-end proof.
-Qed.
-
-Require Import Reals Field.
-(*Coercion INR: nat >->R.
-Coercion IZR: Z >->R.*)
-
-Open Scope R_scope.
-
-Lemma square_abs_square:
-  forall p,(INR (Z.abs_nat p) * INR (Z.abs_nat p)) = (IZR p * IZR p).
-proof.
-  assume p:Z.
-  per cases on p.
-    suppose it is (0%Z).
-      thus thesis.
-    suppose it is (Zpos z).
-      thus thesis.
-    suppose it is (Zneg z).
-      have ((INR (Z.abs_nat (Zneg z)) * INR (Z.abs_nat (Zneg z))) =
-      (IZR (Zpos z) * IZR (Zpos z))).
-           ~= ((- IZR (Zpos z)) * (- IZR (Zpos z))).
-      thus ~= (IZR (Zneg z) * IZR (Zneg z)).
-  end cases.
-end proof.
-Qed.
-
-Definition irrational (x:R):Prop :=
-  forall (p:Z) (q:nat),q<>0%nat -> x<> (IZR p/INR q).
-
-Theorem irrationnal_sqrt_2: irrational (sqrt (INR 2%nat)).
-proof.
-  let p:Z,q:nat be such that H:(q<>0%nat)
-                         and H0:(sqrt (INR 2%nat)=(IZR p/INR q)).
-  have H_in_R:(INR q<>0:>R) by H.
-  have triv:((IZR p/INR q* INR q) =IZR p :>R) by * using field.
-  have sqrt2:((sqrt (INR 2%nat) * sqrt (INR 2%nat))= INR 2%nat:>R) by sqrt_def.
-  have (INR (Z.abs_nat p * Z.abs_nat p)
-     = (INR (Z.abs_nat p) * INR (Z.abs_nat p)))
-    by mult_INR.
-    ~=  (IZR p* IZR p) by square_abs_square.
-    ~=  ((IZR p/INR q*INR q)*(IZR p/INR q*INR q)) by triv. (* we have to factor because field is too weak *)
-    ~=  ((IZR p/INR q)*(IZR p/INR q)*(INR q*INR q)) using ring.
-    ~=  (sqrt (INR 2%nat) * sqrt (INR 2%nat)*(INR q*INR q)) by H0.
-    ~= (INR (2%nat * (q*q)))  by sqrt2,mult_INR.
-  then  (Z.abs_nat p * Z.abs_nat p = 2* (q * q))%nat.
-    ~= ((q*q)+(q*q))%nat.
-    ~= (Div2.double (q*q)).
-  then (q=0%nat) by main_theorem.
-  hence thesis by H.
-end proof.
-Qed.
diff --git a/test-suite/success/decl_mode2.v b/test-suite/success/decl_mode2.v
deleted file mode 100644
index 46174e481..000000000
--- a/test-suite/success/decl_mode2.v
+++ /dev/null
@@ -1,249 +0,0 @@
-Theorem this_is_trivial: True.
-proof.
-  thus thesis.
-end proof.
-Qed.
-
-Theorem T: (True /\ True) /\ True.
-  split. split.
-proof. (* first subgoal *)
-  thus thesis.
-end proof.
-trivial. (* second subgoal *)
-proof. (* third subgoal *)
-  thus thesis.
-end proof.
-Abort.
-
-Theorem this_is_not_so_trivial: False.
-proof.
-end proof. (* here a warning is issued *)
-Fail Qed. (* fails: the proof in incomplete *)
-Admitted. (* Oops! *)
-
-Theorem T: True.
-proof.
-escape.
-auto.
-return.
-Abort.
-
-Theorem T: let a:=false in let b:= true in ( if a then True else False -> if b then True else False).
-intros a b.
-proof.
-assume H:(if a then True else False).
-reconsider H as False.
-reconsider thesis as True.
-Abort.
-
-Theorem T: forall x, x=2 -> 2+x=4.
-proof.
-let x be such that H:(x=2).
-have H':(2+x=2+2) by H.
-Abort.
-
-Theorem T: forall x, x=2 -> 2+x=4.
-proof.
-let x be such that H:(x=2).
-then (2+x=2+2).
-Abort.
-
-Theorem T: forall x, x=2 -> x + x = x * x.
-proof.
-let x be such that H:(x=2).
-have (4 = 4).
-        ~= (2 * 2).
-        ~= (x * x) by H.
-        =~ (2 + 2).
-        =~ H':(x + x) by H.
-Abort.
-
-Theorem T: forall x, x + x = x * x -> x = 0 \/ x = 2.
-proof.
-let x be such that H:(x + x = x * x).
-claim H':((x - 2) * x = 0).
-thus thesis. 
-end claim.
-Abort.
-
-Theorem T: forall (A B:Prop), A -> B -> A /\ B.
-intros A B HA HB.
-proof.
-hence B.
-Abort.
-
-Theorem T: forall (A B C:Prop), A -> B -> C -> A /\ B /\ C.
-intros A B C HA HB HC.
-proof.
-thus B by HB.
-Abort.
-
-Theorem T: forall (A B C:Prop), A -> B -> C -> A /\ B.
-intros A B C HA HB HC.
-proof.
-Fail hence C. (* fails *)
-Abort.
-
-Theorem T: forall (A B:Prop), B -> A \/ B.
-intros A B HB.
-proof.
-hence B.
-Abort.
-
-Theorem T: forall (A B C D:Prop), C -> D -> (A /\ B) \/ (C /\ D).
-intros A B C D HC HD.
-proof.
-thus C by HC.
-Abort.
-
-Theorem T: forall (P:nat -> Prop), P 2 -> exists x,P x.
-intros P HP.
-proof.
-take 2.
-Abort.
-
-Theorem T: forall (P:nat -> Prop), P 2 -> exists x,P x.
-intros P HP.
-proof.
-hence (P 2).
-Abort.
-
-Theorem T: forall (P:nat -> Prop) (R:nat -> nat -> Prop), P 2 -> R 0 2 -> exists x, exists y, P y /\ R x y.
-intros P R HP HR.
-proof.
-thus (P 2) by HP.
-Abort.
-
-Theorem T: forall (A B:Prop) (P:nat -> Prop), (forall x, P x -> B) -> A -> A /\ B.
-intros A B P HP HA.
-proof.
-suffices to have x such that HP':(P x) to show B by HP,HP'.
-Abort.
-
-Theorem T: forall (A:Prop) (P:nat -> Prop), P 2 -> A -> A /\ (forall x, x = 2 -> P x).
-intros A P HP HA.
-proof.
-(* BUG: the next line fails when it should succeed.
-Waiting for someone to investigate the bug.
-focus on (forall x, x = 2 -> P x).
-let x be such that (x = 2).
-hence thesis by HP.
-end focus.
-*)
-Abort.
-
-Theorem T: forall x, x = 0 -> x + x = x * x.
-proof.
-let x be such that H:(x = 0).
-define sqr x as (x * x).
-reconsider thesis as (x + x = sqr x).
-Abort.
-
-Theorem T: forall (P:nat -> Prop), forall x, P x -> P x.
-proof.
-let P:(nat -> Prop).
-let x:nat.
-assume HP:(P x).
-Abort.
-
-Theorem T: forall (P:nat -> Prop), forall x, P x -> P x.
-proof.
-let P:(nat -> Prop).
-Fail let x. (* fails because x's type is not clear *) 
-let x be such that HP:(P x). (* here x's type is inferred from (P x) *)
-Abort.
-
-Theorem T: forall (P:nat -> Prop), forall x, P x -> P x -> P x.
-proof.
-let P:(nat -> Prop).
-let x:nat.
-assume (P x). (* temporary name created *)
-Abort.
-
-Theorem T: forall (P:nat -> Prop), forall x, P x -> P x.
-proof.
-let P:(nat -> Prop).
-let x be such that (P x). (* temporary name created *)
-Abort.
-
-Theorem T: forall (P:nat -> Prop) (A:Prop), (exists x, (P x /\ A)) -> A.
-proof.
-let P:(nat -> Prop),A:Prop be such that H:(exists x, P x /\ A).
-consider x such that HP:(P x) and HA:A from H.
-Abort.
-
-(* Here is an example with pairs: *)
-
-Theorem T: forall p:(nat * nat)%type, (fst p >= snd p) \/ (fst p < snd p).
-proof.
-let p:(nat * nat)%type.
-consider x:nat,y:nat from p.
-reconsider thesis as (x >= y \/ x < y). 
-Abort.
-
-Theorem T: forall P:(nat -> Prop), (forall n, P n -> P (n - 1)) -> 
-(exists m, P m) -> P 0.
-proof.
-let P:(nat -> Prop) be such that HP:(forall n, P n -> P (n - 1)).
-given m such that Hm:(P m).  
-Abort.
-
-Theorem T: forall (A B C:Prop), (A -> C) -> (B -> C) -> (A \/ B) -> C.
-proof.
-let A:Prop,B:Prop,C:Prop be such that HAC:(A -> C) and HBC:(B -> C).
-assume HAB:(A \/ B).
-per cases on HAB.
-suppose A.
-  hence thesis by HAC.
-suppose HB:B.
-  thus thesis by HB,HBC.
-end cases.
-Abort.
-
-Section Coq.
-
-Hypothesis EM : forall P:Prop, P \/ ~ P.
-
-Theorem T: forall (A C:Prop), (A -> C) -> (~A -> C) -> C.
-proof.
-let A:Prop,C:Prop be such that HAC:(A -> C) and HNAC:(~A -> C).
-per cases of (A \/ ~A) by EM.
-suppose (~A).
-  hence thesis by HNAC.
-suppose A.
-  hence thesis by HAC.
-end cases.
-Abort.
-
-Theorem T: forall (A C:Prop), (A -> C) -> (~A -> C) -> C.
-proof.
-let A:Prop,C:Prop be such that HAC:(A -> C) and HNAC:(~A -> C).
-per cases on (EM A).
-suppose (~A).
-Abort.
-End Coq.
-
-Theorem T: forall (A B:Prop) (x:bool), (if x then A else B) -> A \/ B.
-proof.
-let A:Prop,B:Prop,x:bool.
-per cases on x.
-suppose it is true.
-  assume A.
-  hence A.
-suppose it is false.
-  assume B.
-  hence B.
-end cases.
-Abort.
-
-Theorem T: forall (n:nat), n + 0 = n.
-proof.
-let n:nat.
-per induction on n.
-suppose it is 0.
-  thus (0 + 0 = 0).
-suppose it is (S m) and H:thesis for m.
-  then (S (m + 0) = S m).
-  thus =~ (S m + 0).
-end induction.
-Abort.
\ No newline at end of file