1 files changed, 0 insertions, 182 deletions
diff --git a/contrib/micromega/Env.v b/contrib/micromega/Env.v
deleted file mode 100644
index 40db9e46..00000000
--- a/contrib/micromega/Env.v
+++ /dev/null
@@ -1,182 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-(*                                                                      *)
-(* Micromega: A reflexive tactic using the Positivstellensatz           *)
-(*                                                                      *)
-(*  Frédéric Besson (Irisa/Inria) 2006-2008                             *)
-(*                                                                      *)
-(************************************************************************)
-
-Require Import ZArith.
-Require Import Coq.Arith.Max.
-Require Import List.
-Set Implicit Arguments.
-
-(* I have addded a Leaf constructor to the varmap data structure (/contrib/ring/Quote.v) 
-   -- this is harmless and spares a lot of Empty.
-   This means smaller proof-terms. 
-   BTW, by dropping the  polymorphism, I get small (yet noticeable) speed-up.
-*)
-
-Section S.
-
-  Variable D :Type.
-
-  Definition Env := positive -> D.
-
-  Definition jump  (j:positive) (e:Env) := fun x => e (Pplus x j).
-
-  Definition nth  (n:positive) (e : Env ) := e n.
-
-  Definition hd (x:D)  (e: Env)  := nth xH e.
-
-  Definition tail (e: Env) := jump xH e.
-
-  Lemma psucc : forall p,  (match p with
-                              | xI y' => xO (Psucc y')
-                              | xO y' => xI y'
-                              | 1%positive => 2%positive 
-                            end) = (p+1)%positive.
-  Proof.
-    destruct p.
-    auto with zarith.
-    rewrite xI_succ_xO.
-    auto with zarith.
-    reflexivity.
-  Qed.
-
-  Lemma jump_Pplus : forall i j l, 
-    forall x, jump (i + j) l x = jump i (jump j l) x.
-  Proof.
-    unfold jump.
-    intros.
-    rewrite Pplus_assoc.
-    reflexivity.
-  Qed.
-
-  Lemma jump_simpl : forall p l,
-    forall x, jump p l x = 
-    match p with
-      | xH => tail l x
-      | xO p => jump p (jump p l) x
-      | xI p  => jump p (jump p (tail l)) x
-    end.
-  Proof.
-    destruct p ; unfold tail ; intros ;  repeat rewrite <- jump_Pplus.
-    (* xI p = p + p + 1 *)
-    rewrite xI_succ_xO.
-    rewrite Pplus_diag.
-    rewrite <- Pplus_one_succ_r.
-    reflexivity.
-    (* xO p = p + p *)
-    rewrite Pplus_diag.
-    reflexivity.
-    reflexivity.
-  Qed.
-
-  Ltac jump_s :=
-    repeat 
-      match goal with
-        | |- context [jump xH ?e] => rewrite (jump_simpl xH)
-        | |- context [jump (xO ?p) ?e] => rewrite (jump_simpl (xO p))
-        | |- context [jump (xI ?p) ?e] => rewrite (jump_simpl (xI p))
-      end.
-    
-  Lemma jump_tl : forall j l, forall x, tail (jump j l) x = jump j (tail l) x.
-  Proof. 
-    unfold tail.
-    intros.
-    repeat rewrite <- jump_Pplus.
-    rewrite Pplus_comm.
-    reflexivity.
-  Qed.
-
-  Lemma jump_Psucc : forall j l, 
-    forall x, (jump (Psucc j) l x) = (jump 1 (jump j l) x).
-  Proof.
-    intros.
-    rewrite <- jump_Pplus.
-    rewrite Pplus_one_succ_r.
-    rewrite Pplus_comm.
-    reflexivity.
-  Qed.
-
-  Lemma jump_Pdouble_minus_one : forall i l,
-    forall x, (jump (Pdouble_minus_one i) (tail l)) x = (jump i (jump i l)) x.
-  Proof.
-    unfold tail.
-    intros.
-    repeat rewrite <- jump_Pplus.
-    rewrite <- Pplus_one_succ_r.
-    rewrite Psucc_o_double_minus_one_eq_xO.
-    rewrite Pplus_diag.
-    reflexivity.
-  Qed.
-
-  Lemma jump_x0_tail : forall p l, forall x, jump (xO p) (tail l) x = jump (xI p) l x.
-  Proof.
-    intros.
-    unfold jump.
-    unfold tail.
-    unfold jump.
-    rewrite <- Pplus_assoc.
-    simpl.
-    reflexivity.
-  Qed.
-
-  Lemma nth_spec : forall p l x, 
-    nth p l = 
-    match p with
-      | xH => hd x l
-      | xO p => nth p (jump p l)
-      | xI p => nth p (jump p (tail l))
-    end. 
-  Proof.
-    unfold nth.
-    destruct p.
-    intros.
-    unfold jump, tail.
-    unfold jump.
-    rewrite Pplus_diag.
-    rewrite xI_succ_xO.
-    simpl.
-    reflexivity.
-    unfold jump.
-    rewrite Pplus_diag.
-    reflexivity.
-    unfold hd.
-    unfold nth.
-    reflexivity.
-  Qed.
-
-
-  Lemma nth_jump : forall p l x, nth p (tail l) = hd x (jump p l).
-  Proof.
-    unfold tail.
-    unfold hd.
-    unfold jump.
-    unfold nth.
-    intros.
-    rewrite Pplus_comm.
-    reflexivity.
-  Qed.
-
-  Lemma nth_Pdouble_minus_one :
-    forall p l, nth (Pdouble_minus_one p) (tail l) = nth p (jump p l).
-  Proof.
-    intros.
-    unfold tail.
-    unfold nth, jump.
-    rewrite Pplus_diag.
-    rewrite <- Psucc_o_double_minus_one_eq_xO.
-    rewrite Pplus_one_succ_r.
-    reflexivity.
-  Qed.
-
-End S.
-