From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001
From: Stephane Glondu
Date: Thu, 12 Jan 2012 16:02:20 +0100
Subject: Imported Upstream version 8.4~beta
---
plugins/setoid_ring/Algebra_syntax.v | 25 ++
plugins/setoid_ring/ArithRing.v | 6 +-
plugins/setoid_ring/BinList.v | 2 +-
plugins/setoid_ring/Cring.v | 272 +++++++++++++++
plugins/setoid_ring/Field.v | 2 +-
plugins/setoid_ring/Field_tac.v | 2 +-
plugins/setoid_ring/Field_theory.v | 132 +++-----
plugins/setoid_ring/InitialRing.v | 122 +++----
plugins/setoid_ring/Integral_domain.v | 44 +++
plugins/setoid_ring/NArithRing.v | 4 +-
plugins/setoid_ring/Ncring.v | 305 +++++++++++++++++
plugins/setoid_ring/Ncring_initial.v | 221 ++++++++++++
plugins/setoid_ring/Ncring_polynom.v | 621 ++++++++++++++++++++++++++++++++++
plugins/setoid_ring/Ncring_tac.v | 308 +++++++++++++++++
plugins/setoid_ring/Ring.v | 2 +-
plugins/setoid_ring/Ring_base.v | 2 +-
plugins/setoid_ring/Ring_polynom.v | 24 +-
plugins/setoid_ring/Ring_theory.v | 19 +-
plugins/setoid_ring/Rings_Q.v | 30 ++
plugins/setoid_ring/Rings_R.v | 34 ++
plugins/setoid_ring/Rings_Z.v | 14 +
plugins/setoid_ring/ZArithRing.v | 8 +-
plugins/setoid_ring/newring.ml4 | 69 ++--
plugins/setoid_ring/vo.itarget | 10 +
24 files changed, 2045 insertions(+), 233 deletions(-)
create mode 100644 plugins/setoid_ring/Algebra_syntax.v
create mode 100644 plugins/setoid_ring/Cring.v
create mode 100644 plugins/setoid_ring/Integral_domain.v
create mode 100644 plugins/setoid_ring/Ncring.v
create mode 100644 plugins/setoid_ring/Ncring_initial.v
create mode 100644 plugins/setoid_ring/Ncring_polynom.v
create mode 100644 plugins/setoid_ring/Ncring_tac.v
create mode 100644 plugins/setoid_ring/Rings_Q.v
create mode 100644 plugins/setoid_ring/Rings_R.v
create mode 100644 plugins/setoid_ring/Rings_Z.v
(limited to 'plugins/setoid_ring')
diff --git a/plugins/setoid_ring/Algebra_syntax.v b/plugins/setoid_ring/Algebra_syntax.v
new file mode 100644
index 00000000..e896554e
--- /dev/null
+++ b/plugins/setoid_ring/Algebra_syntax.v
@@ -0,0 +1,25 @@
+
+Class Zero (A : Type) := zero : A.
+Notation "0" := zero.
+Class One (A : Type) := one : A.
+Notation "1" := one.
+Class Addition (A : Type) := addition : A -> A -> A.
+Notation "_+_" := addition.
+Notation "x + y" := (addition x y).
+Class Multiplication {A B : Type} := multiplication : A -> B -> B.
+Notation "_*_" := multiplication.
+Notation "x * y" := (multiplication x y).
+Class Subtraction (A : Type) := subtraction : A -> A -> A.
+Notation "_-_" := subtraction.
+Notation "x - y" := (subtraction x y).
+Class Opposite (A : Type) := opposite : A -> A.
+Notation "-_" := opposite.
+Notation "- x" := (opposite(x)).
+Class Equality {A : Type}:= equality : A -> A -> Prop.
+Notation "_==_" := equality.
+Notation "x == y" := (equality x y) (at level 70, no associativity).
+Class Bracket (A B: Type):= bracket : A -> B.
+Notation "[ x ]" := (bracket(x)).
+Class Power {A B: Type} := power : A -> B -> A.
+Notation "x ^ y" := (power x y).
+
diff --git a/plugins/setoid_ring/ArithRing.v b/plugins/setoid_ring/ArithRing.v
index 6998b656..06822ae1 100644
--- a/plugins/setoid_ring/ArithRing.v
+++ b/plugins/setoid_ring/ArithRing.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* idtac
+ | ?e1::?e2::_ =>
+ match goal with
+ |- (?op ?u1 ?u2) =>
+ change (op
+ (@Ring_polynom.PEeval
+ _ zero _+_ _*_ _-_ -_ Z Ncring_initial.gen_phiZ N (fun n:N => n)
+ (@Ring_theory.pow_N _ 1 multiplication) lvar e1)
+ (@Ring_polynom.PEeval
+ _ zero _+_ _*_ _-_ -_ Z Ncring_initial.gen_phiZ N (fun n:N => n)
+ (@Ring_theory.pow_N _ 1 multiplication) lvar e2))
+ end
+ end.
+
+Section cring.
+Context {R:Type}`{Rr:Cring R}.
+
+Lemma cring_eq_ext: ring_eq_ext _+_ _*_ -_ _==_.
+intros. apply mk_reqe;intros.
+rewrite H. rewrite H0. reflexivity.
+rewrite H. rewrite H0. reflexivity.
+ rewrite H. reflexivity. Defined.
+
+Lemma cring_almost_ring_theory:
+ almost_ring_theory (R:=R) zero one _+_ _*_ _-_ -_ _==_.
+intros. apply mk_art ;intros.
+rewrite ring_add_0_l; reflexivity.
+rewrite ring_add_comm; reflexivity.
+rewrite ring_add_assoc; reflexivity.
+rewrite ring_mul_1_l; reflexivity.
+apply ring_mul_0_l.
+rewrite cring_mul_comm; reflexivity.
+rewrite ring_mul_assoc; reflexivity.
+rewrite ring_distr_l; reflexivity.
+rewrite ring_opp_mul_l; reflexivity.
+apply ring_opp_add.
+rewrite ring_sub_def ; reflexivity. Defined.
+
+Lemma cring_morph:
+ ring_morph zero one _+_ _*_ _-_ -_ _==_
+ 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool
+ Ncring_initial.gen_phiZ.
+intros. apply mkmorph ; intros; simpl; try reflexivity.
+rewrite Ncring_initial.gen_phiZ_add; reflexivity.
+rewrite ring_sub_def. unfold Zminus. rewrite Ncring_initial.gen_phiZ_add.
+rewrite Ncring_initial.gen_phiZ_opp; reflexivity.
+rewrite Ncring_initial.gen_phiZ_mul; reflexivity.
+rewrite Ncring_initial.gen_phiZ_opp; reflexivity.
+rewrite (Zeqb_ok x y H). reflexivity. Defined.
+
+Lemma cring_power_theory :
+ @Ring_theory.power_theory R one _*_ _==_ N (fun n:N => n)
+ (@Ring_theory.pow_N _ 1 multiplication).
+intros; apply Ring_theory.mkpow_th. reflexivity. Defined.
+
+Lemma cring_div_theory:
+ div_theory _==_ Zplus Zmult Ncring_initial.gen_phiZ Z.quotrem.
+intros. apply InitialRing.Ztriv_div_th. unfold Setoid_Theory.
+simpl. apply ring_setoid. Defined.
+
+End cring.
+
+Ltac cring_gen :=
+ match goal with
+ |- ?g => let lterm := lterm_goal g in
+ match eval red in (list_reifyl (lterm:=lterm)) with
+ | (?fv, ?lexpr) =>
+ (*idtac "variables:";idtac fv;
+ idtac "terms:"; idtac lterm;
+ idtac "reifications:"; idtac lexpr; *)
+ reify_goal fv lexpr lterm;
+ match goal with
+ |- ?g =>
+ generalize
+ (@Ring_polynom.ring_correct _ 0 1 _+_ _*_ _-_ -_ _==_
+ ring_setoid
+ cring_eq_ext
+ cring_almost_ring_theory
+ Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool
+ Ncring_initial.gen_phiZ
+ cring_morph
+ N
+ (fun n:N => n)
+ (@Ring_theory.pow_N _ 1 multiplication)
+ cring_power_theory
+ Z.quotrem
+ cring_div_theory
+ O fv nil);
+ let rc := fresh "rc"in
+ intro rc; apply rc
+ end
+ end
+ end.
+
+Ltac cring_compute:= vm_compute; reflexivity.
+
+Ltac cring:=
+ intros;
+ cring_gen;
+ cring_compute.
+
+Instance Zcri: (Cring (Rr:=Zr)).
+red. exact Zmult_comm. Defined.
+
+(* Cring_simplify *)
+
+Ltac cring_simplify_aux lterm fv lexpr hyp :=
+ match lterm with
+ | ?t0::?lterm =>
+ match lexpr with
+ | ?e::?le =>
+ let t := constr:(@Ring_polynom.norm_subst
+ Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool Z.quotrem O nil e) in
+ let te :=
+ constr:(@Ring_polynom.Pphi_dev
+ _ 0 1 _+_ _*_ _-_ -_
+
+ Z 0%Z 1%Z Zeq_bool
+ Ncring_initial.gen_phiZ
+ get_signZ fv t) in
+ let eq1 := fresh "ring" in
+ let nft := eval vm_compute in t in
+ let t':= fresh "t" in
+ pose (t' := nft);
+ assert (eq1 : t = t');
+ [vm_cast_no_check (refl_equal t')|
+ let eq2 := fresh "ring" in
+ assert (eq2:(@Ring_polynom.PEeval
+ _ zero _+_ _*_ _-_ -_ Z Ncring_initial.gen_phiZ N (fun n:N => n)
+ (@Ring_theory.pow_N _ 1 multiplication) fv e) == te);
+ [let eq3 := fresh "ring" in
+ generalize (@ring_rw_correct _ 0 1 _+_ _*_ _-_ -_ _==_
+ ring_setoid
+ cring_eq_ext
+ cring_almost_ring_theory
+ Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool
+ Ncring_initial.gen_phiZ
+ cring_morph
+ N
+ (fun n:N => n)
+ (@Ring_theory.pow_N _ 1 multiplication)
+ cring_power_theory
+ Z.quotrem
+ cring_div_theory
+ get_signZ get_signZ_th
+ O nil fv I nil (refl_equal nil) );
+ intro eq3; apply eq3; reflexivity|
+ match hyp with
+ | 1%nat => rewrite eq2
+ | ?H => try rewrite eq2 in H
+ end];
+ let P:= fresh "P" in
+ match hyp with
+ | 1%nat =>
+ rewrite eq1;
+ pattern (@Ring_polynom.Pphi_dev
+ _ 0 1 _+_ _*_ _-_ -_
+
+ Z 0%Z 1%Z Zeq_bool
+ Ncring_initial.gen_phiZ
+ get_signZ fv t');
+ match goal with
+ |- (?p ?t) => set (P:=p)
+ end;
+ unfold t' in *; clear t' eq1 eq2;
+ unfold Pphi_dev, Pphi_avoid; simpl;
+ repeat (unfold mkmult1, mkmultm1, mkmult_c_pos, mkmult_c,
+ mkadd_mult, mkmult_c_pos, mkmult_pow, mkadd_mult,
+ mkpow;simpl)
+ | ?H =>
+ rewrite eq1 in H;
+ pattern (@Ring_polynom.Pphi_dev
+ _ 0 1 _+_ _*_ _-_ -_
+
+ Z 0%Z 1%Z Zeq_bool
+ Ncring_initial.gen_phiZ
+ get_signZ fv t') in H;
+ match type of H with
+ | (?p ?t) => set (P:=p) in H
+ end;
+ unfold t' in *; clear t' eq1 eq2;
+ unfold Pphi_dev, Pphi_avoid in H; simpl in H;
+ repeat (unfold mkmult1, mkmultm1, mkmult_c_pos, mkmult_c,
+ mkadd_mult, mkmult_c_pos, mkmult_pow, mkadd_mult,
+ mkpow in H;simpl in H)
+ end; unfold P in *; clear P
+ ]; cring_simplify_aux lterm fv le hyp
+ | nil => idtac
+ end
+ | nil => idtac
+ end.
+
+Ltac set_variables fv :=
+ match fv with
+ | nil => idtac
+ | ?t::?fv =>
+ let v := fresh "X" in
+ set (v:=t) in *; set_variables fv
+ end.
+
+Ltac deset n:=
+ match n with
+ | 0%nat => idtac
+ | S ?n1 =>
+ match goal with
+ | h:= ?v : ?t |- ?g => unfold h in *; clear h; deset n1
+ end
+ end.
+
+(* a est soit un terme de l'anneau, soit une liste de termes.
+J'ai pas réussi à un décomposer les Vlists obtenues avec ne_constr_list
+ dans Tactic Notation *)
+
+Ltac cring_simplify_gen a hyp :=
+ let lterm :=
+ match a with
+ | _::_ => a
+ | _ => constr:(a::nil)
+ end in
+ match eval red in (list_reifyl (lterm:=lterm)) with
+ | (?fv, ?lexpr) => idtac lterm; idtac fv; idtac lexpr;
+ let n := eval compute in (length fv) in
+ idtac n;
+ let lt:=fresh "lt" in
+ set (lt:= lterm);
+ let lv:=fresh "fv" in
+ set (lv:= fv);
+ (* les termes de fv sont remplacés par des variables
+ pour pouvoir utiliser simpl ensuite sans risquer
+ des simplifications indésirables *)
+ set_variables fv;
+ let lterm1 := eval unfold lt in lt in
+ let lv1 := eval unfold lv in lv in
+ idtac lterm1; idtac lv1;
+ cring_simplify_aux lterm1 lv1 lexpr hyp;
+ clear lt lv;
+ (* on remet les termes de fv *)
+ deset n
+ end.
+
+Tactic Notation "cring_simplify" constr(lterm):=
+ cring_simplify_gen lterm 1%nat.
+
+Tactic Notation "cring_simplify" constr(lterm) "in" ident(H):=
+ cring_simplify_gen lterm H.
+
diff --git a/plugins/setoid_ring/Field.v b/plugins/setoid_ring/Field.v
index 6a755af2..90f2f497 100644
--- a/plugins/setoid_ring/Field.v
+++ b/plugins/setoid_ring/Field.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* Cpow.
Variable rpow : R -> Cpow -> R.
Variable pow_th : power_theory rI rmul req Cp_phi rpow.
@@ -390,52 +390,16 @@ Qed.
***************************************************************************)
-Fixpoint positive_eq (p1 p2 : positive) {struct p1} : bool :=
- match p1, p2 with
- xH, xH => true
- | xO p3, xO p4 => positive_eq p3 p4
- | xI p3, xI p4 => positive_eq p3 p4
- | _, _ => false
- end.
-
-Theorem positive_eq_correct:
- forall p1 p2, if positive_eq p1 p2 then p1 = p2 else p1 <> p2.
-intros p1; elim p1;
- (try (intros p2; case p2; simpl; auto; intros; discriminate)).
-intros p3 rec p2; case p2; simpl; auto; (try (intros; discriminate)); intros p4.
-generalize (rec p4); case (positive_eq p3 p4); auto.
-intros H1; apply f_equal with ( f := xI ); auto.
-intros H1 H2; case H1; injection H2; auto.
-intros p3 rec p2; case p2; simpl; auto; (try (intros; discriminate)); intros p4.
-generalize (rec p4); case (positive_eq p3 p4); auto.
-intros H1; apply f_equal with ( f := xO ); auto.
-intros H1 H2; case H1; injection H2; auto.
-Qed.
-
-Definition N_eq n1 n2 :=
- match n1, n2 with
- | N0, N0 => true
- | Npos p1, Npos p2 => positive_eq p1 p2
- | _, _ => false
- end.
-
-Lemma N_eq_correct : forall n1 n2, if N_eq n1 n2 then n1 = n2 else n1 <> n2.
-Proof.
- intros [ |p1] [ |p2];simpl;trivial;try(intro H;discriminate H;fail).
- assert (H:=positive_eq_correct p1 p2);destruct (positive_eq p1 p2);
- [rewrite H;trivial | intro H1;injection H1;subst;apply H;trivial].
-Qed.
-
(* equality test *)
Fixpoint PExpr_eq (e1 e2 : PExpr C) {struct e1} : bool :=
match e1, e2 with
PEc c1, PEc c2 => ceqb c1 c2
- | PEX p1, PEX p2 => positive_eq p1 p2
+ | PEX p1, PEX p2 => Pos.eqb p1 p2
| PEadd e3 e5, PEadd e4 e6 => if PExpr_eq e3 e4 then PExpr_eq e5 e6 else false
| PEsub e3 e5, PEsub e4 e6 => if PExpr_eq e3 e4 then PExpr_eq e5 e6 else false
| PEmul e3 e5, PEmul e4 e6 => if PExpr_eq e3 e4 then PExpr_eq e5 e6 else false
| PEopp e3, PEopp e4 => PExpr_eq e3 e4
- | PEpow e3 n3, PEpow e4 n4 => if N_eq n3 n4 then PExpr_eq e3 e4 else false
+ | PEpow e3 n3, PEpow e4 n4 => if N.eqb n3 n4 then PExpr_eq e3 e4 else false
| _, _ => false
end.
@@ -460,8 +424,7 @@ intros l e1; elim e1.
intros c1; intros e2; elim e2; simpl; (try (intros; discriminate)).
intros c2; apply (morph_eq CRmorph).
intros p1; intros e2; elim e2; simpl; (try (intros; discriminate)).
-intros p2; generalize (positive_eq_correct p1 p2); case (positive_eq p1 p2);
- (try (intros; discriminate)); intros H; rewrite H; auto.
+intros p2; case Pos.eqb_spec; intros; now subst.
intros e3 rec1 e5 rec2 e2; case e2; simpl; (try (intros; discriminate)).
intros e4 e6; generalize (rec1 e4); case (PExpr_eq e3 e4);
(try (intros; discriminate)); generalize (rec2 e6); case (PExpr_eq e5 e6);
@@ -478,9 +441,8 @@ intros e3 rec e2; (case e2; simpl; (try (intros; discriminate))).
intros e4; generalize (rec e4); case (PExpr_eq e3 e4);
(try (intros; discriminate)); auto.
intros e3 rec n3 e2;(case e2;simpl;(try (intros;discriminate))).
-intros e4 n4;generalize (N_eq_correct n3 n4);destruct (N_eq n3 n4);
-intros;try discriminate.
-repeat rewrite pow_th.(rpow_pow_N);rewrite H;rewrite (rec _ H0);auto.
+intros e4 n4; case N.eqb_spec; try discriminate; intros EQ H; subst.
+repeat rewrite pow_th.(rpow_pow_N). rewrite (rec _ H);auto.
Qed.
(* add *)
@@ -507,7 +469,7 @@ Definition NPEpow x n :=
match n with
| N0 => PEc cI
| Npos p =>
- if positive_eq p xH then x else
+ if Pos.eqb p xH then x else
match x with
| PEc c =>
if ceqb c cI then PEc cI else if ceqb c cO then PEc cO else PEc (pow_pos cmul c p)
@@ -520,10 +482,10 @@ Theorem NPEpow_correct : forall l e n,
Proof.
destruct n;simpl.
rewrite pow_th.(rpow_pow_N);simpl;auto.
- generalize (positive_eq_correct p xH).
- destruct (positive_eq p 1);intros.
- rewrite H;rewrite pow_th.(rpow_pow_N). trivial.
- clear H;destruct e;simpl;auto.
+ fold (p =? 1)%positive.
+ case Pos.eqb_spec; intros H; (rewrite H || clear H).
+ now rewrite pow_th.(rpow_pow_N).
+ destruct e;simpl;auto.
repeat apply ceqb_rect;simpl;intros;rewrite pow_th.(rpow_pow_N);simpl.
symmetry;induction p;simpl;trivial; ring [IHp H CRmorph.(morph1)].
symmetry; induction p;simpl;trivial;ring [IHp CRmorph.(morph0)].
@@ -539,7 +501,7 @@ Fixpoint NPEmul (x y : PExpr C) {struct x} : PExpr C :=
| _, PEc c =>
if ceqb c cI then x else if ceqb c cO then PEc cO else PEmul x y
| PEpow e1 n1, PEpow e2 n2 =>
- if N_eq n1 n2 then NPEpow (NPEmul e1 e2) n1 else PEmul x y
+ if N.eqb n1 n2 then NPEpow (NPEmul e1 e2) n1 else PEmul x y
| _, _ => PEmul x y
end.
@@ -554,10 +516,10 @@ induction e1;destruct e2; simpl in |- *;try reflexivity;
try (intro eq_c; rewrite eq_c in |- *); simpl in |- *; try reflexivity;
try ring [(morph0 CRmorph) (morph1 CRmorph)].
apply (morph_mul CRmorph).
-assert (H:=N_eq_correct n n0);destruct (N_eq n n0).
+case N.eqb_spec; intros H; try rewrite <- H; clear H.
rewrite NPEpow_correct. simpl.
repeat rewrite pow_th.(rpow_pow_N).
-rewrite IHe1;rewrite <- H;destruct n;simpl;try ring.
+rewrite IHe1; destruct n;simpl;try ring.
apply pow_pos_mul.
simpl;auto.
Qed.
@@ -760,6 +722,14 @@ Fixpoint isIn (e1:PExpr C) (p1:positive)
Notation pow_pos_plus := (Ring_theory.pow_pos_Pplus _ Rsth Reqe.(Rmul_ext)
ARth.(ARmul_comm) ARth.(ARmul_assoc)).
+ Lemma Z_pos_sub_gt : forall p q, (p > q)%positive ->
+ Z.pos_sub p q = Zpos (p - q).
+ Proof.
+ intros. apply Z.pos_sub_gt. now apply Pos.gt_lt.
+ Qed.
+
+ Ltac simpl_pos_sub := rewrite ?Z_pos_sub_gt in * by assumption.
+
Lemma isIn_correct_aux : forall l e1 e2 p1 p2,
match
(if PExpr_eq e1 e2 then
@@ -779,10 +749,12 @@ Fixpoint isIn (e1:PExpr C) (p1:positive)
Proof.
intros l e1 e2 p1 p2; generalize (PExpr_eq_semi_correct l e1 e2);
case (PExpr_eq e1 e2); simpl; auto; intros H.
- case_eq ((p1 ?= p2)%positive Eq);intros;simpl.
+ rewrite Z.pos_sub_spec.
+ case_eq ((p1 ?= p2)%positive);intros;simpl.
repeat rewrite pow_th.(rpow_pow_N);simpl. split. 2:refine (refl_equal _).
rewrite (Pcompare_Eq_eq _ _ H0).
rewrite H by trivial. ring [ (morph1 CRmorph)].
+ fold (p2 - p1 =? 1)%positive.
fold (NPEpow e2 (Npos (p2 - p1))).
rewrite NPEpow_correct;simpl.
repeat rewrite pow_th.(rpow_pow_N);simpl.
@@ -790,22 +762,17 @@ Proof.
rewrite <- pow_pos_plus; rewrite Pplus_minus;auto. apply ZC2;trivial.
repeat rewrite pow_th.(rpow_pow_N);simpl.
rewrite H;trivial.
- change (ZtoN
- match (p1 ?= p1 - p2)%positive Eq with
- | Eq => 0
- | Lt => Zneg (p1 - p2 - p1)
- | Gt => Zpos (p1 - (p1 - p2))
- end) with (ZtoN (Zpos p1 - Zpos (p1 -p2))).
+ change (Z.pos_sub p1 (p1-p2)) with (Zpos p1 - Zpos (p1 -p2))%Z.
replace (Zpos (p1 - p2)) with (Zpos p1 - Zpos p2)%Z.
split.
repeat rewrite Zth.(Rsub_def). rewrite (Ring_theory.Ropp_add Zsth Zeqe Zth).
- rewrite Zplus_assoc. simpl. rewrite Pcompare_refl. simpl.
+ rewrite Zplus_assoc, Z.add_opp_diag_r. simpl.
ring [ (morph1 CRmorph)].
assert (Zpos p1 > 0 /\ Zpos p2 > 0)%Z. split;refine (refl_equal _).
apply Zplus_gt_reg_l with (Zpos p2).
rewrite Zplus_minus. change (Zpos p2 + Zpos p1 > 0 + Zpos p1)%Z.
apply Zplus_gt_compat_r. refine (refl_equal _).
- simpl;rewrite H0;trivial.
+ simpl. now simpl_pos_sub.
Qed.
Lemma pow_pos_pow_pos : forall x p1 p2, pow_pos rmul (pow_pos rmul x p1) p2 == pow_pos rmul x (p1*p2).
@@ -835,7 +802,7 @@ destruct n.
destruct n;simpl.
rewrite NPEmul_correct;repeat rewrite pow_th.(rpow_pow_N);simpl.
intros (H1,H2) (H3,H4).
- unfold Zgt in H2, H4;simpl in H2,H4. rewrite H4 in H3;simpl in H3.
+ simpl_pos_sub. simpl in H3.
rewrite pow_pos_mul. rewrite H1;rewrite H3.
assert (pow_pos rmul (NPEeval l e1) (p1 - p4) * NPEeval l p3 *
(pow_pos rmul (NPEeval l e1) p4 * NPEeval l p5) ==
@@ -845,11 +812,10 @@ destruct n.
split. symmetry;apply ARth.(ARmul_assoc). refine (refl_equal _). trivial.
repeat rewrite pow_th.(rpow_pow_N);simpl.
intros (H1,H2) (H3,H4).
- unfold Zgt in H2, H4;simpl in H2,H4. rewrite H4 in H3;simpl in H3.
- rewrite H2 in H1;simpl in H1.
+ simpl_pos_sub. simpl in H1, H3.
assert (Zpos p1 > Zpos p6)%Z.
apply Zgt_trans with (Zpos p4). exact H4. exact H2.
- unfold Zgt in H;simpl in H;rewrite H.
+ simpl_pos_sub.
split. 2:exact H.
rewrite pow_pos_mul. simpl;rewrite H1;rewrite H3.
assert (pow_pos rmul (NPEeval l e1) (p1 - p4) * NPEeval l p3 *
@@ -863,11 +829,11 @@ destruct n.
(Zpos p1 - Zpos p6 = Zpos p1 - Zpos p4 + (Zpos p4 - Zpos p6))%Z.
change ((Zpos p1 - Zpos p6)%Z = (Zpos p1 + (- Zpos p4) + (Zpos p4 +(- Zpos p6)))%Z).
rewrite <- Zplus_assoc. rewrite (Zplus_assoc (- Zpos p4)).
- simpl. rewrite Pcompare_refl. simpl. reflexivity.
+ simpl. rewrite Z.pos_sub_diag. simpl. reflexivity.
unfold Zminus, Zopp in H0. simpl in H0.
- rewrite H2 in H0;rewrite H4 in H0;rewrite H in H0. inversion H0;trivial.
+ simpl_pos_sub. inversion H0; trivial.
simpl. repeat rewrite pow_th.(rpow_pow_N).
- intros H1 (H2,H3). unfold Zgt in H3;simpl in H3. rewrite H3 in H2;rewrite H3.
+ intros H1 (H2,H3). simpl_pos_sub.
rewrite NPEmul_correct;simpl;rewrite NPEpow_correct;simpl.
simpl in H2. rewrite pow_th.(rpow_pow_N);simpl.
rewrite pow_pos_mul. split. ring [H2]. exact H3.
@@ -878,8 +844,7 @@ destruct n.
rewrite NPEmul_correct;simpl;rewrite NPEpow_correct;simpl.
repeat rewrite pow_th.(rpow_pow_N);simpl. rewrite pow_pos_mul.
intros (H1, H2);rewrite H1;split.
- unfold Zgt in H2;simpl in H2;rewrite H2;rewrite H2 in H1.
- simpl in H1;ring [H1]. trivial.
+ simpl_pos_sub. simpl in H1;ring [H1]. trivial.
trivial.
destruct n. trivial.
generalize (H p1 (p0*p2)%positive);clear H;destruct (isIn e1 p1 p (p0*p2)). destruct p3.
@@ -937,8 +902,7 @@ Proof.
repeat rewrite NPEpow_correct;simpl;
repeat rewrite pow_th.(rpow_pow_N);simpl).
intros (H, Hgt);split;try ring [H CRmorph.(morph1)].
- intros (H, Hgt). unfold Zgt in Hgt;simpl in Hgt;rewrite Hgt in H.
- simpl in H;split;try ring [H].
+ intros (H, Hgt). simpl_pos_sub. simpl in H;split;try ring [H].
rewrite <- pow_pos_plus. rewrite Pplus_minus. reflexivity. trivial.
simpl;intros. repeat rewrite NPEmul_correct;simpl.
rewrite NPEpow_correct;simpl. split;ring [CRmorph.(morph1)].
@@ -1805,25 +1769,24 @@ Lemma gen_phiPOS_inj : forall x y,
x = y.
intros x y.
repeat rewrite <- (same_gen Rsth Reqe ARth) in |- *.
-ElimPcompare x y; intro.
+case (Pos.compare_spec x y).
+ intros.
+ trivial.
intros.
- apply Pcompare_Eq_eq; trivial.
- intro.
elim gen_phiPOS_not_0 with (y - x)%positive.
apply add_inj_r with x.
symmetry in |- *.
rewrite (ARadd_0_r Rsth ARth) in |- *.
rewrite <- (ARgen_phiPOS_add Rsth Reqe ARth) in |- *.
rewrite Pplus_minus in |- *; trivial.
- change Eq with (CompOpp Eq) in |- *.
- rewrite <- Pcompare_antisym in |- *; trivial.
- rewrite H in |- *; trivial.
- intro.
+ now apply Pos.lt_gt.
+ intros.
elim gen_phiPOS_not_0 with (x - y)%positive.
apply add_inj_r with y.
rewrite (ARadd_0_r Rsth ARth) in |- *.
rewrite <- (ARgen_phiPOS_add Rsth Reqe ARth) in |- *.
rewrite Pplus_minus in |- *; trivial.
+ now apply Pos.lt_gt.
Qed.
@@ -1841,12 +1804,9 @@ Qed.
Lemma gen_phiN_complete : forall x y,
gen_phiN rO rI radd rmul x == gen_phiN rO rI radd rmul y ->
- Neq_bool x y = true.
-intros.
- replace y with x.
- unfold Neq_bool in |- *.
- rewrite Ncompare_refl in |- *; trivial.
- apply gen_phiN_inj; trivial.
+ N.eqb x y = true.
+Proof.
+intros. now apply N.eqb_eq, gen_phiN_inj.
Qed.
End AlmostField.
diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v
index 026e70c8..763dbe7b 100644
--- a/plugins/setoid_ring/InitialRing.v
+++ b/plugins/setoid_ring/InitialRing.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* Z0
- | Lt => Zneg (y - x)
- | Gt => Zpos (x - y)
- end
- == gen_phiPOS1 x + -gen_phiPOS1 y.
+ Lemma gen_phiZ1_pos_sub : forall x y,
+ gen_phiZ1 (Z.pos_sub x y) == gen_phiPOS1 x + -gen_phiPOS1 y.
Proof.
intros x y.
- assert (H:= (Pcompare_Eq_eq x y)); assert (H0 := Pminus_mask_Gt x y).
- generalize (Pminus_mask_Gt y x).
- replace Eq with (CompOpp Eq);[intro H1;simpl|trivial].
- rewrite <- Pcompare_antisym in H1.
- destruct ((x ?= y)%positive Eq).
- rewrite H;trivial. rewrite (Ropp_def Rth);rrefl.
- destruct H1 as [h [Heq1 [Heq2 Hor]]];trivial.
- unfold Pminus; rewrite Heq1;rewrite <- Heq2.
+ rewrite Z.pos_sub_spec.
+ case Pos.compare_spec; intros H; simpl.
+ rewrite H. rewrite (Ropp_def Rth);rrefl.
+ rewrite <- (Pos.sub_add y x H) at 2. rewrite Pos.add_comm.
rewrite (ARgen_phiPOS_add ARth);simpl;norm.
rewrite (Ropp_def Rth);norm.
- destruct H0 as [h [Heq1 [Heq2 Hor]]];trivial.
- unfold Pminus; rewrite Heq1;rewrite <- Heq2.
+ rewrite <- (Pos.sub_add x y H) at 2.
rewrite (ARgen_phiPOS_add ARth);simpl;norm.
- add_push (gen_phiPOS1 h);rewrite (Ropp_def Rth); norm.
+ add_push (gen_phiPOS1 (x-y));rewrite (Ropp_def Rth); norm.
Qed.
- Lemma match_compOpp : forall x (B:Type) (be bl bg:B),
- match CompOpp x with Eq => be | Lt => bl | Gt => bg end
- = match x with Eq => be | Lt => bg | Gt => bl end.
- Proof. destruct x;simpl;intros;trivial. Qed.
-
Lemma gen_phiZ_add : forall x y, [x + y] == [x] + [y].
Proof.
intros x y; repeat rewrite same_genZ; generalize x y;clear x y.
- induction x;destruct y;simpl;norm.
+ destruct x, y; simpl; norm.
apply (ARgen_phiPOS_add ARth).
- apply gen_phiZ1_add_pos_neg.
- replace Eq with (CompOpp Eq);trivial.
- rewrite <- Pcompare_antisym;simpl.
- rewrite match_compOpp.
- rewrite (Radd_comm Rth).
- apply gen_phiZ1_add_pos_neg.
+ apply gen_phiZ1_pos_sub.
+ rewrite gen_phiZ1_pos_sub. apply (Radd_comm Rth).
rewrite (ARgen_phiPOS_add ARth); norm.
Qed.
@@ -244,47 +223,28 @@ End ZMORPHISM.
Lemma Nsth : Setoid_Theory N (@eq N).
Proof (Eqsth N).
-Lemma Nseqe : sring_eq_ext Nplus Nmult (@eq N).
-Proof (Eq_s_ext Nplus Nmult).
+Lemma Nseqe : sring_eq_ext N.add N.mul (@eq N).
+Proof (Eq_s_ext N.add N.mul).
-Lemma Nth : semi_ring_theory N0 (Npos xH) Nplus Nmult (@eq N).
+Lemma Nth : semi_ring_theory 0%N 1%N N.add N.mul (@eq N).
Proof.
- constructor. exact Nplus_0_l. exact Nplus_comm. exact Nplus_assoc.
- exact Nmult_1_l. exact Nmult_0_l. exact Nmult_comm. exact Nmult_assoc.
- exact Nmult_plus_distr_r.
+ constructor. exact N.add_0_l. exact N.add_comm. exact N.add_assoc.
+ exact N.mul_1_l. exact N.mul_0_l. exact N.mul_comm. exact N.mul_assoc.
+ exact N.mul_add_distr_r.
Qed.
-Definition Nsub := SRsub Nplus.
+Definition Nsub := SRsub N.add.
Definition Nopp := (@SRopp N).
-Lemma Neqe : ring_eq_ext Nplus Nmult Nopp (@eq N).
+Lemma Neqe : ring_eq_ext N.add N.mul Nopp (@eq N).
Proof (SReqe_Reqe Nseqe).
Lemma Nath :
- almost_ring_theory N0 (Npos xH) Nplus Nmult Nsub Nopp (@eq N).
+ almost_ring_theory 0%N 1%N N.add N.mul Nsub Nopp (@eq N).
Proof (SRth_ARth Nsth Nth).
-Definition Neq_bool (x y:N) :=
- match Ncompare x y with
- | Eq => true
- | _ => false
- end.
-
-Lemma Neq_bool_ok : forall x y, Neq_bool x y = true -> x = y.
- Proof.
- intros x y;unfold Neq_bool.
- assert (H:=Ncompare_Eq_eq x y);
- destruct (Ncompare x y);intros;try discriminate.
- rewrite H;trivial.
- Qed.
-
-Lemma Neq_bool_complete : forall x y, Neq_bool x y = true -> x = y.
- Proof.
- intros x y;unfold Neq_bool.
- assert (H:=Ncompare_Eq_eq x y);
- destruct (Ncompare x y);intros;try discriminate.
- rewrite H;trivial.
- Qed.
+Lemma Neqb_ok : forall x y, N.eqb x y = true -> x = y.
+Proof. exact (fun x y => proj1 (N.eqb_eq x y)). Qed.
(**Same as above : definition of two,extensionaly equal, generic morphisms *)
(**from N to any semi-ring*)
@@ -307,9 +267,7 @@ Section NMORPHISM.
Notation "x == y" := (req x y).
Add Morphism radd : radd_ext4. exact (Radd_ext Reqe). Qed.
Add Morphism rmul : rmul_ext4. exact (Rmul_ext Reqe). Qed.
- Add Morphism ropp : ropp_ext4. exact (Ropp_ext Reqe). Qed.
- Add Morphism rsub : rsub_ext5. exact (ARsub_ext Rsth Reqe ARth). Qed.
- Ltac norm := gen_srewrite Rsth Reqe ARth.
+ Ltac norm := gen_srewrite_sr Rsth Reqe ARth.
Definition gen_phiN1 x :=
match x with
@@ -326,8 +284,8 @@ Section NMORPHISM.
Lemma same_genN : forall x, [x] == gen_phiN1 x.
Proof.
- destruct x;simpl. rrefl.
- rewrite (same_gen Rsth Reqe ARth);rrefl.
+ destruct x;simpl. reflexivity.
+ now rewrite (same_gen Rsth Reqe ARth).
Qed.
Lemma gen_phiN_add : forall x y, [x + y] == [x] + [y].
@@ -349,11 +307,11 @@ Section NMORPHISM.
(*gen_phiN satisfies morphism specifications*)
Lemma gen_phiN_morph : ring_morph 0 1 radd rmul rsub ropp req
- N0 (Npos xH) Nplus Nmult Nsub Nopp Neq_bool gen_phiN.
+ 0%N 1%N N.add N.mul Nsub Nopp N.eqb gen_phiN.
Proof.
- constructor;intros;simpl; try rrefl.
- apply gen_phiN_add. apply gen_phiN_sub. apply gen_phiN_mult.
- rewrite (Neq_bool_ok x y);trivial. rrefl.
+ constructor; simpl; try reflexivity.
+ apply gen_phiN_add. apply gen_phiN_sub. apply gen_phiN_mult.
+ intros x y EQ. apply N.eqb_eq in EQ. now subst.
Qed.
End NMORPHISM.
@@ -402,7 +360,7 @@ Fixpoint Nw_is0 (w : Nword) : bool :=
Fixpoint Nweq_bool (w1 w2 : Nword) {struct w1} : bool :=
match w1, w2 with
| n1::w1', n2::w2' =>
- if Neq_bool n1 n2 then Nweq_bool w1' w2' else false
+ if N.eqb n1 n2 then Nweq_bool w1' w2' else false
| nil, _ => Nw_is0 w2
| _, nil => Nw_is0 w1
end.
@@ -486,10 +444,10 @@ induction w1; intros.
simpl in H.
rewrite gen_phiNword_cons in |- *.
- case_eq (Neq_bool a n); intros.
+ case_eq (N.eqb a n); intros H0.
rewrite H0 in H.
- rewrite <- (Neq_bool_ok _ _ H0) in |- *.
- rewrite (IHw1 _ H) in |- *.
+ apply N.eqb_eq in H0. rewrite <- H0.
+ rewrite (IHw1 _ H).
reflexivity.
rewrite H0 in H; discriminate H.
@@ -632,19 +590,19 @@ Qed.
Variable zphi : Z -> R.
- Lemma Ztriv_div_th : div_theory req Zplus Zmult zphi ZOdiv_eucl.
+ Lemma Ztriv_div_th : div_theory req Z.add Z.mul zphi Z.quotrem.
Proof.
constructor.
- intros; generalize (ZOdiv_eucl_correct a b); case ZOdiv_eucl; intros; subst.
- rewrite Zmult_comm; rsimpl.
+ intros; generalize (Z.quotrem_eq a b); case Z.quotrem; intros; subst.
+ rewrite Z.mul_comm; rsimpl.
Qed.
Variable nphi : N -> R.
- Lemma Ntriv_div_th : div_theory req Nplus Nmult nphi Ndiv_eucl.
+ Lemma Ntriv_div_th : div_theory req N.add N.mul nphi N.div_eucl.
constructor.
- intros; generalize (Ndiv_eucl_correct a b); case Ndiv_eucl; intros; subst.
- rewrite Nmult_comm; rsimpl.
+ intros; generalize (N.div_eucl_spec a b); case N.div_eucl; intros; subst.
+ rewrite N.mul_comm; rsimpl.
Qed.
End GEN_DIV.
diff --git a/plugins/setoid_ring/Integral_domain.v b/plugins/setoid_ring/Integral_domain.v
new file mode 100644
index 00000000..5a224e38
--- /dev/null
+++ b/plugins/setoid_ring/Integral_domain.v
@@ -0,0 +1,44 @@
+Require Export Cring.
+
+
+(* Definition of integral domains: commutative ring without zero divisor *)
+
+Class Integral_domain {R : Type}`{Rcr:Cring R} := {
+ integral_domain_product:
+ forall x y, x * y == 0 -> x == 0 \/ y == 0;
+ integral_domain_one_zero: not (1 == 0)}.
+
+Section integral_domain.
+
+Context {R:Type}`{Rid:Integral_domain R}.
+
+Lemma integral_domain_minus_one_zero: ~ - (1:R) == 0.
+red;intro. apply integral_domain_one_zero.
+assert (0 == - (0:R)). cring.
+rewrite H0. rewrite <- H. cring.
+Qed.
+
+
+Definition pow (r : R) (n : nat) := Ring_theory.pow_N 1 mul r (N_of_nat n).
+
+Lemma pow_not_zero: forall p n, pow p n == 0 -> p == 0.
+induction n. unfold pow; simpl. intros. absurd (1 == 0).
+simpl. apply integral_domain_one_zero.
+ trivial. setoid_replace (pow p (S n)) with (p * (pow p n)).
+intros.
+case (integral_domain_product p (pow p n) H). trivial. trivial.
+unfold pow; simpl.
+clear IHn. induction n; simpl; try cring.
+ rewrite Ring_theory.pow_pos_Psucc. cring. apply ring_setoid.
+apply ring_mult_comp.
+apply cring_mul_comm.
+apply ring_mul_assoc.
+Qed.
+
+Lemma Rintegral_domain_pow:
+ forall c p r, ~c == 0 -> c * (pow p r) == ring0 -> p == ring0.
+intros. case (integral_domain_product c (pow p r) H0). intros; absurd (c == ring0); auto.
+intros. apply pow_not_zero with r. trivial. Qed.
+
+End integral_domain.
+
diff --git a/plugins/setoid_ring/NArithRing.v b/plugins/setoid_ring/NArithRing.v
index 8d7cb0ea..fafd16ab 100644
--- a/plugins/setoid_ring/NArithRing.v
+++ b/plugins/setoid_ring/NArithRing.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* constr:NotConstant
end.
-Add Ring Nr : Nth (decidable Neq_bool_ok, constants [Ncst]).
+Add Ring Nr : Nth (decidable Neqb_ok, constants [Ncst]).
diff --git a/plugins/setoid_ring/Ncring.v b/plugins/setoid_ring/Ncring.v
new file mode 100644
index 00000000..9a30fa47
--- /dev/null
+++ b/plugins/setoid_ring/Ncring.v
@@ -0,0 +1,305 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* T->T}
+ {mul:T->T->T}
+ {sub:T->T->T}
+ {opp:T->T}
+ {ring_eq:T->T->Prop}.
+
+Instance zero_notation(T:Type)`{Ring_ops T}:Zero T:= ring0.
+Instance one_notation(T:Type)`{Ring_ops T}:One T:= ring1.
+Instance add_notation(T:Type)`{Ring_ops T}:Addition T:= add.
+Instance mul_notation(T:Type)`{Ring_ops T}:@Multiplication T T:= mul.
+Instance sub_notation(T:Type)`{Ring_ops T}:Subtraction T:= sub.
+Instance opp_notation(T:Type)`{Ring_ops T}:Opposite T:= opp.
+Instance eq_notation(T:Type)`{Ring_ops T}:@Equality T:= ring_eq.
+
+Class Ring `{Ro:Ring_ops}:={
+ ring_setoid: Equivalence _==_;
+ ring_plus_comp: Proper (_==_ ==> _==_ ==>_==_) _+_;
+ ring_mult_comp: Proper (_==_ ==> _==_ ==>_==_) _*_;
+ ring_sub_comp: Proper (_==_ ==> _==_ ==>_==_) _-_;
+ ring_opp_comp: Proper (_==_==>_==_) -_;
+ ring_add_0_l : forall x, 0 + x == x;
+ ring_add_comm : forall x y, x + y == y + x;
+ ring_add_assoc : forall x y z, x + (y + z) == (x + y) + z;
+ ring_mul_1_l : forall x, 1 * x == x;
+ ring_mul_1_r : forall x, x * 1 == x;
+ ring_mul_assoc : forall x y z, x * (y * z) == (x * y) * z;
+ ring_distr_l : forall x y z, (x + y) * z == x * z + y * z;
+ ring_distr_r : forall x y z, z * ( x + y) == z * x + z * y;
+ ring_sub_def : forall x y, x - y == x + -y;
+ ring_opp_def : forall x, x + -x == 0
+}.
+(* inutile! je sais plus pourquoi j'ai mis ca...
+Instance ring_Ring_ops(R:Type)`{Ring R}
+ :@Ring_ops R 0 1 addition multiplication subtraction opposite equality.
+*)
+Existing Instance ring_setoid.
+Existing Instance ring_plus_comp.
+Existing Instance ring_mult_comp.
+Existing Instance ring_sub_comp.
+Existing Instance ring_opp_comp.
+
+Section Ring_power.
+
+Context {R:Type}`{Ring R}.
+
+ Fixpoint pow_pos (x:R) (i:positive) {struct i}: R :=
+ match i with
+ | xH => x
+ | xO i => let p := pow_pos x i in p * p
+ | xI i => let p := pow_pos x i in x * (p * p)
+ end.
+
+ Definition pow_N (x:R) (p:N) :=
+ match p with
+ | N0 => 1
+ | Npos p => pow_pos x p
+ end.
+
+End Ring_power.
+
+Definition ZN(x:Z):=
+ match x with
+ Z0 => N0
+ |Zpos p | Zneg p => Npos p
+end.
+
+Instance power_ring {R:Type}`{Ring R} : Power:=
+ {power x y := pow_N x (ZN y)}.
+
+(** Interpretation morphisms definition*)
+
+Class Ring_morphism (C R:Type)`{Cr:Ring C} `{Rr:Ring R}`{Rh:Bracket C R}:= {
+ ring_morphism0 : [0] == 0;
+ ring_morphism1 : [1] == 1;
+ ring_morphism_add : forall x y, [x + y] == [x] + [y];
+ ring_morphism_sub : forall x y, [x - y] == [x] - [y];
+ ring_morphism_mul : forall x y, [x * y] == [x] * [y];
+ ring_morphism_opp : forall x, [-x] == -[x];
+ ring_morphism_eq : forall x y, x == y -> [x] == [y]}.
+
+Section Ring.
+
+Context {R:Type}`{Rr:Ring R}.
+
+(* Powers *)
+
+ Lemma pow_pos_comm : forall x j, x * pow_pos x j == pow_pos x j * x.
+induction j; simpl. rewrite <- ring_mul_assoc.
+rewrite <- ring_mul_assoc.
+rewrite <- IHj. rewrite (ring_mul_assoc (pow_pos x j) x (pow_pos x j)).
+rewrite <- IHj. rewrite <- ring_mul_assoc. reflexivity.
+rewrite <- ring_mul_assoc. rewrite <- IHj.
+rewrite ring_mul_assoc. rewrite IHj.
+rewrite <- ring_mul_assoc. rewrite IHj. reflexivity. reflexivity.
+Qed.
+
+ Lemma pow_pos_Psucc : forall x j, pow_pos x (Psucc j) == x * pow_pos x j.
+ Proof.
+ induction j; simpl.
+ rewrite IHj.
+rewrite <- (ring_mul_assoc x (pow_pos x j) (x * pow_pos x j)).
+rewrite (ring_mul_assoc (pow_pos x j) x (pow_pos x j)).
+ rewrite <- pow_pos_comm.
+rewrite <- ring_mul_assoc. reflexivity.
+reflexivity. reflexivity.
+Qed.
+
+ Lemma pow_pos_Pplus : forall x i j,
+ pow_pos x (i + j) == pow_pos x i * pow_pos x j.
+ Proof.
+ intro x;induction i;intros.
+ rewrite xI_succ_xO;rewrite Pplus_one_succ_r.
+ rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc.
+ repeat rewrite IHi.
+ rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;
+ rewrite pow_pos_Psucc.
+ simpl;repeat rewrite ring_mul_assoc. reflexivity.
+ rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc.
+ repeat rewrite IHi. rewrite ring_mul_assoc. reflexivity.
+ rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;rewrite pow_pos_Psucc.
+ simpl. reflexivity.
+ Qed.
+
+ Definition id_phi_N (x:N) : N := x.
+
+ Lemma pow_N_pow_N : forall x n, pow_N x (id_phi_N n) == pow_N x n.
+ Proof.
+ intros; reflexivity.
+ Qed.
+
+ (** Identity is a morphism *)
+ (*
+ Instance IDmorph : Ring_morphism _ _ _ (fun x => x).
+ Proof.
+ apply (Build_Ring_morphism H6 H6 (fun x => x));intros;
+ try reflexivity. trivial.
+ Qed.
+*)
+ (** rings are almost rings*)
+ Lemma ring_mul_0_l : forall x, 0 * x == 0.
+ Proof.
+ intro x. setoid_replace (0*x) with ((0+1)*x + -x).
+ rewrite ring_add_0_l. rewrite ring_mul_1_l .
+ rewrite ring_opp_def . fold zero. reflexivity.
+ rewrite ring_distr_l . rewrite ring_mul_1_l .
+ rewrite <- ring_add_assoc ; rewrite ring_opp_def .
+ rewrite ring_add_comm ; rewrite ring_add_0_l ;reflexivity.
+ Qed.
+
+ Lemma ring_mul_0_r : forall x, x * 0 == 0.
+ Proof.
+ intro x; setoid_replace (x*0) with (x*(0+1) + -x).
+ rewrite ring_add_0_l ; rewrite ring_mul_1_r .
+ rewrite ring_opp_def ; fold zero; reflexivity.
+
+ rewrite ring_distr_r ;rewrite ring_mul_1_r .
+ rewrite <- ring_add_assoc ; rewrite ring_opp_def .
+ rewrite ring_add_comm ; rewrite ring_add_0_l ;reflexivity.
+ Qed.
+
+ Lemma ring_opp_mul_l : forall x y, -(x * y) == -x * y.
+ Proof.
+ intros x y;rewrite <- (ring_add_0_l (- x * y)).
+ rewrite ring_add_comm .
+ rewrite <- (ring_opp_def (x*y)).
+ rewrite ring_add_assoc .
+ rewrite <- ring_distr_l.
+ rewrite (ring_add_comm (-x));rewrite ring_opp_def .
+ rewrite ring_mul_0_l;rewrite ring_add_0_l ;reflexivity.
+ Qed.
+
+Lemma ring_opp_mul_r : forall x y, -(x * y) == x * -y.
+ Proof.
+ intros x y;rewrite <- (ring_add_0_l (x * - y)).
+ rewrite ring_add_comm .
+ rewrite <- (ring_opp_def (x*y)).
+ rewrite ring_add_assoc .
+ rewrite <- ring_distr_r .
+ rewrite (ring_add_comm (-y));rewrite ring_opp_def .
+ rewrite ring_mul_0_r;rewrite ring_add_0_l ;reflexivity.
+ Qed.
+
+ Lemma ring_opp_add : forall x y, -(x + y) == -x + -y.
+ Proof.
+ intros x y;rewrite <- (ring_add_0_l (-(x+y))).
+ rewrite <- (ring_opp_def x).
+ rewrite <- (ring_add_0_l (x + - x + - (x + y))).
+ rewrite <- (ring_opp_def y).
+ rewrite (ring_add_comm x).
+ rewrite (ring_add_comm y).
+ rewrite <- (ring_add_assoc (-y)).
+ rewrite <- (ring_add_assoc (- x)).
+ rewrite (ring_add_assoc y).
+ rewrite (ring_add_comm y).
+ rewrite <- (ring_add_assoc (- x)).
+ rewrite (ring_add_assoc y).
+ rewrite (ring_add_comm y);rewrite ring_opp_def .
+ rewrite (ring_add_comm (-x) 0);rewrite ring_add_0_l .
+ rewrite ring_add_comm; reflexivity.
+ Qed.
+
+ Lemma ring_opp_opp : forall x, - -x == x.
+ Proof.
+ intros x; rewrite <- (ring_add_0_l (- -x)).
+ rewrite <- (ring_opp_def x).
+ rewrite <- ring_add_assoc ; rewrite ring_opp_def .
+ rewrite (ring_add_comm x); rewrite ring_add_0_l . reflexivity.
+ Qed.
+
+ Lemma ring_sub_ext :
+ forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 - y1 == x2 - y2.
+ Proof.
+ intros.
+ setoid_replace (x1 - y1) with (x1 + -y1).
+ setoid_replace (x2 - y2) with (x2 + -y2).
+ rewrite H;rewrite H0;reflexivity.
+ rewrite ring_sub_def. reflexivity.
+ rewrite ring_sub_def. reflexivity.
+ Qed.
+
+ Ltac mrewrite :=
+ repeat first
+ [ rewrite ring_add_0_l
+ | rewrite <- (ring_add_comm 0)
+ | rewrite ring_mul_1_l
+ | rewrite ring_mul_0_l
+ | rewrite ring_distr_l
+ | reflexivity
+ ].
+
+ Lemma ring_add_0_r : forall x, (x + 0) == x.
+ Proof. intros; mrewrite. Qed.
+
+
+ Lemma ring_add_assoc1 : forall x y z, (x + y) + z == (y + z) + x.
+ Proof.
+ intros;rewrite <- (ring_add_assoc x).
+ rewrite (ring_add_comm x);reflexivity.
+ Qed.
+
+ Lemma ring_add_assoc2 : forall x y z, (y + x) + z == (y + z) + x.
+ Proof.
+ intros; repeat rewrite <- ring_add_assoc.
+ rewrite (ring_add_comm x); reflexivity.
+ Qed.
+
+ Lemma ring_opp_zero : -0 == 0.
+ Proof.
+ rewrite <- (ring_mul_0_r 0). rewrite ring_opp_mul_l.
+ repeat rewrite ring_mul_0_r. reflexivity.
+ Qed.
+
+End Ring.
+
+(** Some simplification tactics*)
+Ltac gen_reflexivity := reflexivity.
+
+Ltac gen_rewrite :=
+ repeat first
+ [ reflexivity
+ | progress rewrite ring_opp_zero
+ | rewrite ring_add_0_l
+ | rewrite ring_add_0_r
+ | rewrite ring_mul_1_l
+ | rewrite ring_mul_1_r
+ | rewrite ring_mul_0_l
+ | rewrite ring_mul_0_r
+ | rewrite ring_distr_l
+ | rewrite ring_distr_r
+ | rewrite ring_add_assoc
+ | rewrite ring_mul_assoc
+ | progress rewrite ring_opp_add
+ | progress rewrite ring_sub_def
+ | progress rewrite <- ring_opp_mul_l
+ | progress rewrite <- ring_opp_mul_r ].
+
+Ltac gen_add_push x :=
+repeat (match goal with
+ | |- context [(?y + x) + ?z] =>
+ progress rewrite (ring_add_assoc2 x y z)
+ | |- context [(x + ?y) + ?z] =>
+ progress rewrite (ring_add_assoc1 x y z)
+ end).
diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v
new file mode 100644
index 00000000..3c79f7d9
--- /dev/null
+++ b/plugins/setoid_ring/Ncring_initial.v
@@ -0,0 +1,221 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* 1
+ | xO p => (1 + 1) * (gen_phiPOS1 p)
+ | xI p => 1 + ((1 + 1) * (gen_phiPOS1 p))
+ end.
+
+ Fixpoint gen_phiPOS (p:positive) : R :=
+ match p with
+ | xH => 1
+ | xO xH => (1 + 1)
+ | xO p => (1 + 1) * (gen_phiPOS p)
+ | xI xH => 1 + (1 +1)
+ | xI p => 1 + ((1 + 1) * (gen_phiPOS p))
+ end.
+
+ Definition gen_phiZ1 z :=
+ match z with
+ | Zpos p => gen_phiPOS1 p
+ | Z0 => 0
+ | Zneg p => -(gen_phiPOS1 p)
+ end.
+
+ Definition gen_phiZ z :=
+ match z with
+ | Zpos p => gen_phiPOS p
+ | Z0 => 0
+ | Zneg p => -(gen_phiPOS p)
+ end.
+ Notation "[ x ]" := (gen_phiZ x).
+
+ Definition get_signZ z :=
+ match z with
+ | Zneg p => Some (Zpos p)
+ | _ => None
+ end.
+
+ Ltac norm := gen_rewrite.
+ Ltac add_push := Ncring.gen_add_push.
+Ltac rsimpl := simpl.
+
+ Lemma same_gen : forall x, gen_phiPOS1 x == gen_phiPOS x.
+ Proof.
+ induction x;rsimpl.
+ rewrite IHx. destruct x;simpl;norm.
+ rewrite IHx;destruct x;simpl;norm.
+ reflexivity.
+ Qed.
+
+ Lemma ARgen_phiPOS_Psucc : forall x,
+ gen_phiPOS1 (Psucc x) == 1 + (gen_phiPOS1 x).
+ Proof.
+ induction x;rsimpl;norm.
+ rewrite IHx. gen_rewrite. add_push 1. reflexivity.
+ Qed.
+
+ Lemma ARgen_phiPOS_add : forall x y,
+ gen_phiPOS1 (x + y) == (gen_phiPOS1 x) + (gen_phiPOS1 y).
+ Proof.
+ induction x;destruct y;simpl;norm.
+ rewrite Pplus_carry_spec.
+ rewrite ARgen_phiPOS_Psucc.
+ rewrite IHx;norm.
+ add_push (gen_phiPOS1 y);add_push 1;reflexivity.
+ rewrite IHx;norm;add_push (gen_phiPOS1 y);reflexivity.
+ rewrite ARgen_phiPOS_Psucc;norm;add_push 1;reflexivity.
+ rewrite IHx;norm;add_push(gen_phiPOS1 y); add_push 1;reflexivity.
+ rewrite IHx;norm;add_push(gen_phiPOS1 y);reflexivity.
+ add_push 1;reflexivity.
+ rewrite ARgen_phiPOS_Psucc;norm;add_push 1;reflexivity.
+ Qed.
+
+ Lemma ARgen_phiPOS_mult :
+ forall x y, gen_phiPOS1 (x * y) == gen_phiPOS1 x * gen_phiPOS1 y.
+ Proof.
+ induction x;intros;simpl;norm.
+ rewrite ARgen_phiPOS_add;simpl;rewrite IHx;norm.
+ rewrite IHx;reflexivity.
+ Qed.
+
+
+(*morphisms are extensionaly equal*)
+ Lemma same_genZ : forall x, [x] == gen_phiZ1 x.
+ Proof.
+ destruct x;rsimpl; try rewrite same_gen; reflexivity.
+ Qed.
+
+ Lemma gen_Zeqb_ok : forall x y,
+ Zeq_bool x y = true -> [x] == [y].
+ Proof.
+ intros x y H7.
+ assert (H10 := Zeq_bool_eq x y H7);unfold IDphi in H10.
+ rewrite H10;reflexivity.
+ Qed.
+
+ Lemma gen_phiZ1_add_pos_neg : forall x y,
+ gen_phiZ1 (Z.pos_sub x y)
+ == gen_phiPOS1 x + -gen_phiPOS1 y.
+ Proof.
+ intros x y.
+ rewrite Z.pos_sub_spec.
+ assert (HH0 := Pminus_mask_Gt x y). unfold Pos.gt in HH0.
+ assert (HH1 := Pminus_mask_Gt y x). unfold Pos.gt in HH1.
+ rewrite Pos.compare_antisym in HH1.
+ destruct (Pos.compare_spec x y) as [HH|HH|HH].
+ subst. rewrite ring_opp_def;reflexivity.
+ destruct HH1 as [h [HHeq1 [HHeq2 HHor]]];trivial.
+ unfold Pminus; rewrite HHeq1;rewrite <- HHeq2.
+ rewrite ARgen_phiPOS_add;simpl;norm.
+ rewrite ring_opp_def;norm.
+ destruct HH0 as [h [HHeq1 [HHeq2 HHor]]];trivial.
+ unfold Pminus; rewrite HHeq1;rewrite <- HHeq2.
+ rewrite ARgen_phiPOS_add;simpl;norm.
+ add_push (gen_phiPOS1 h). rewrite ring_opp_def ; norm.
+ Qed.
+
+ Lemma match_compOpp : forall x (B:Type) (be bl bg:B),
+ match CompOpp x with Eq => be | Lt => bl | Gt => bg end
+ = match x with Eq => be | Lt => bg | Gt => bl end.
+ Proof. destruct x;simpl;intros;trivial. Qed.
+
+ Lemma gen_phiZ_add : forall x y, [x + y] == [x] + [y].
+ Proof.
+ intros x y; repeat rewrite same_genZ; generalize x y;clear x y.
+ induction x;destruct y;simpl;norm.
+ apply ARgen_phiPOS_add.
+ apply gen_phiZ1_add_pos_neg.
+ rewrite gen_phiZ1_add_pos_neg. rewrite ring_add_comm.
+reflexivity.
+ rewrite ARgen_phiPOS_add. rewrite ring_opp_add. reflexivity.
+Qed.
+
+Lemma gen_phiZ_opp : forall x, [- x] == - [x].
+ Proof.
+ intros x. repeat rewrite same_genZ. generalize x ;clear x.
+ induction x;simpl;norm.
+ rewrite ring_opp_opp. reflexivity.
+ Qed.
+
+ Lemma gen_phiZ_mul : forall x y, [x * y] == [x] * [y].
+ Proof.
+ intros x y;repeat rewrite same_genZ.
+ destruct x;destruct y;simpl;norm;
+ rewrite ARgen_phiPOS_mult;try (norm;fail).
+ rewrite ring_opp_opp ;reflexivity.
+ Qed.
+
+ Lemma gen_phiZ_ext : forall x y : Z, x = y -> [x] == [y].
+ Proof. intros;subst;reflexivity. Qed.
+
+(*proof that [.] satisfies morphism specifications*)
+Global Instance gen_phiZ_morph :
+(@Ring_morphism (Z:Type) R _ _ _ _ _ _ _ Zops Zr _ _ _ _ _ _ _ _ _ gen_phiZ) . (* beurk!*)
+ apply Build_Ring_morphism; simpl;try reflexivity.
+ apply gen_phiZ_add. intros. rewrite ring_sub_def.
+replace (Zminus x y) with (x + (-y))%Z. rewrite gen_phiZ_add.
+rewrite gen_phiZ_opp. rewrite ring_sub_def. reflexivity.
+reflexivity.
+ apply gen_phiZ_mul. apply gen_phiZ_opp. apply gen_phiZ_ext.
+ Defined.
+
+End ZMORPHISM.
+
+Instance multiplication_phi_ring{R:Type}`{Ring R} : Multiplication :=
+ {multiplication x y := (gen_phiZ x) * y}.
+
+
diff --git a/plugins/setoid_ring/Ncring_polynom.v b/plugins/setoid_ring/Ncring_polynom.v
new file mode 100644
index 00000000..c0d31587
--- /dev/null
+++ b/plugins/setoid_ring/Ncring_polynom.v
@@ -0,0 +1,621 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* : non commutative polynomials on a commutative ring A *)
+
+Set Implicit Arguments.
+Require Import Setoid.
+Require Import BinList.
+Require Import BinPos.
+Require Import BinNat.
+Require Import BinInt.
+Require Export Ring_polynom. (* n'utilise que PExpr *)
+Require Export Ncring.
+
+Section MakeRingPol.
+
+Context (C R:Type) `{Rh:Ring_morphism C R}.
+
+Variable phiCR_comm: forall (c:C)(x:R), x * [c] == [c] * x.
+
+ Ltac rsimpl := repeat (gen_rewrite || rewrite phiCR_comm).
+ Ltac add_push := gen_add_push .
+
+(* Definition of non commutative multivariable polynomials
+ with coefficients in C :
+ *)
+
+ Inductive Pol : Type :=
+ | Pc : C -> Pol
+ | PX : Pol -> positive -> positive -> Pol -> Pol.
+ (* PX P i n Q represents P * X_i^n + Q *)
+Definition cO:C . exact ring0. Defined.
+Definition cI:C . exact ring1. Defined.
+
+ Definition P0 := Pc 0.
+ Definition P1 := Pc 1.
+
+Variable Ceqb:C->C->bool.
+Class Equalityb (A : Type):= {equalityb : A -> A -> bool}.
+Notation "x =? y" := (equalityb x y) (at level 70, no associativity).
+Variable Ceqb_eq: forall x y:C, Ceqb x y = true -> (x == y).
+
+Instance equalityb_coef : Equalityb C :=
+ {equalityb x y := Ceqb x y}.
+
+ Fixpoint Peq (P P' : Pol) {struct P'} : bool :=
+ match P, P' with
+ | Pc c, Pc c' => c =? c'
+ | PX P i n Q, PX P' i' n' Q' =>
+ match Pcompare i i' Eq, Pcompare n n' Eq with
+ | Eq, Eq => if Peq P P' then Peq Q Q' else false
+ | _,_ => false
+ end
+ | _, _ => false
+ end.
+
+Instance equalityb_pol : Equalityb Pol :=
+ {equalityb x y := Peq x y}.
+
+(* Q a ses variables de queue < i *)
+ Definition mkPX P i n Q :=
+ match P with
+ | Pc c => if c =? 0 then Q else PX P i n Q
+ | PX P' i' n' Q' =>
+ match Pcompare i i' Eq with
+ | Eq => if Q' =? P0 then PX P' i (n + n') Q else PX P i n Q
+ | _ => PX P i n Q
+ end
+ end.
+
+ Definition mkXi i n := PX P1 i n P0.
+
+ Definition mkX i := mkXi i 1.
+
+ (** Opposite of addition *)
+
+ Fixpoint Popp (P:Pol) : Pol :=
+ match P with
+ | Pc c => Pc (- c)
+ | PX P i n Q => PX (Popp P) i n (Popp Q)
+ end.
+
+ Notation "-- P" := (Popp P)(at level 30).
+
+ (** Addition et subtraction *)
+
+ Fixpoint PaddCl (c:C)(P:Pol) {struct P} : Pol :=
+ match P with
+ | Pc c1 => Pc (c + c1)
+ | PX P i n Q => PX P i n (PaddCl c Q)
+ end.
+
+(* Q quelconque *)
+
+Section PaddX.
+Variable Padd:Pol->Pol->Pol.
+Variable P:Pol.
+
+(* Xi^n * P + Q
+les variables de tete de Q ne sont pas forcement < i
+mais Q est normalis : variables de tete decroissantes *)
+
+Fixpoint PaddX (i n:positive)(Q:Pol){struct Q}:=
+ match Q with
+ | Pc c => mkPX P i n Q
+ | PX P' i' n' Q' =>
+ match Pcompare i i' Eq with
+ | (* i > i' *)
+ Gt => mkPX P i n Q
+ | (* i < i' *)
+ Lt => mkPX P' i' n' (PaddX i n Q')
+ | (* i = i' *)
+ Eq => match ZPminus n n' with
+ | (* n > n' *)
+ Zpos k => mkPX (PaddX i k P') i' n' Q'
+ | (* n = n' *)
+ Z0 => mkPX (Padd P P') i n Q'
+ | (* n < n' *)
+ Zneg k => mkPX (Padd P (mkPX P' i k P0)) i n Q'
+ end
+ end
+ end.
+
+End PaddX.
+
+Fixpoint Padd (P1 P2: Pol) {struct P1} : Pol :=
+ match P1 with
+ | Pc c => PaddCl c P2
+ | PX P' i' n' Q' =>
+ PaddX Padd P' i' n' (Padd Q' P2)
+ end.
+
+ Notation "P ++ P'" := (Padd P P').
+
+Definition Psub(P P':Pol):= P ++ (--P').
+
+ Notation "P -- P'" := (Psub P P')(at level 50).
+
+ (** Multiplication *)
+
+ Fixpoint PmulC_aux (P:Pol) (c:C) {struct P} : Pol :=
+ match P with
+ | Pc c' => Pc (c' * c)
+ | PX P i n Q => mkPX (PmulC_aux P c) i n (PmulC_aux Q c)
+ end.
+
+ Definition PmulC P c :=
+ if c =? 0 then P0 else
+ if c =? 1 then P else PmulC_aux P c.
+
+ Fixpoint Pmul (P1 P2 : Pol) {struct P2} : Pol :=
+ match P2 with
+ | Pc c => PmulC P1 c
+ | PX P i n Q =>
+ PaddX Padd (Pmul P1 P) i n (Pmul P1 Q)
+ end.
+
+ Notation "P ** P'" := (Pmul P P')(at level 40).
+
+ Definition Psquare (P:Pol) : Pol := P ** P.
+
+
+ (** Evaluation of a polynomial towards R *)
+
+ Fixpoint Pphi(l:list R) (P:Pol) {struct P} : R :=
+ match P with
+ | Pc c => [c]
+ | PX P i n Q =>
+ let x := nth 0 i l in
+ let xn := pow_pos x n in
+ (Pphi l P) * xn + (Pphi l Q)
+ end.
+
+ Reserved Notation "P @ l " (at level 10, no associativity).
+ Notation "P @ l " := (Pphi l P).
+ (** Proofs *)
+ Lemma ZPminus_spec : forall x y,
+ match ZPminus x y with
+ | Z0 => x = y
+ | Zpos k => x = (y + k)%positive
+ | Zneg k => y = (x + k)%positive
+ end.
+ Proof.
+ induction x;destruct y.
+ replace (ZPminus (xI x) (xI y)) with (Zdouble (ZPminus x y));trivial.
+ assert (Hh := IHx y);destruct (ZPminus x y);unfold Zdouble;
+rewrite Hh;trivial.
+ replace (ZPminus (xI x) (xO y)) with (Zdouble_plus_one (ZPminus x y));
+trivial.
+ assert (Hh := IHx y);destruct (ZPminus x y);unfold Zdouble_plus_one;
+rewrite Hh;trivial.
+ apply Pplus_xI_double_minus_one.
+ simpl;trivial.
+ replace (ZPminus (xO x) (xI y)) with (Zdouble_minus_one (ZPminus x y));
+trivial.
+ assert (Hh := IHx y);destruct (ZPminus x y);unfold Zdouble_minus_one;
+rewrite Hh;trivial.
+ apply Pplus_xI_double_minus_one.
+ replace (ZPminus (xO x) (xO y)) with (Zdouble (ZPminus x y));trivial.
+ assert (Hh := IHx y);destruct (ZPminus x y);unfold Zdouble;rewrite Hh;
+trivial.
+ replace (ZPminus (xO x) xH) with (Zpos (Pdouble_minus_one x));trivial.
+ rewrite <- Pplus_one_succ_l.
+ rewrite Psucc_o_double_minus_one_eq_xO;trivial.
+ replace (ZPminus xH (xI y)) with (Zneg (xO y));trivial.
+ replace (ZPminus xH (xO y)) with (Zneg (Pdouble_minus_one y));trivial.
+ rewrite <- Pplus_one_succ_l.
+ rewrite Psucc_o_double_minus_one_eq_xO;trivial.
+ simpl;trivial.
+ Qed.
+
+ Lemma Peq_ok : forall P P',
+ (P =? P') = true -> forall l, P@l == P'@ l.
+ Proof.
+ induction P;destruct P';simpl;intros;try discriminate;trivial.
+ apply ring_morphism_eq.
+ apply Ceqb_eq ;trivial.
+ assert (H1h := IHP1 P'1);assert (H2h := IHP2 P'2).
+ simpl in H1h. destruct (Peq P2 P'1). simpl in H2h;
+destruct (Peq P3 P'2).
+ rewrite (H1h);trivial . rewrite (H2h);trivial.
+assert (H3h := Pcompare_Eq_eq p p1);
+ destruct (Pos.compare_cont p p1 Eq);
+assert (H4h := Pcompare_Eq_eq p0 p2);
+destruct (Pos.compare_cont p0 p2 Eq); try (discriminate H).
+ rewrite H3h;trivial. rewrite H4h;trivial. reflexivity.
+ destruct (Pos.compare_cont p p1 Eq); destruct (Pos.compare_cont p0 p2 Eq);
+ try (discriminate H).
+ destruct (Pos.compare_cont p p1 Eq); destruct (Pos.compare_cont p0 p2 Eq);
+ try (discriminate H).
+ Qed.
+
+ Lemma Pphi0 : forall l, P0@l == 0.
+ Proof.
+ intros;simpl.
+ rewrite ring_morphism0. reflexivity.
+ Qed.
+
+ Lemma Pphi1 : forall l, P1@l == 1.
+ Proof.
+ intros;simpl; rewrite ring_morphism1. reflexivity.
+ Qed.
+
+ Lemma mkPX_ok : forall l P i n Q,
+ (mkPX P i n Q)@l == P@l * (pow_pos (nth 0 i l) n) + Q@l.
+ Proof.
+ intros l P i n Q;unfold mkPX.
+ destruct P;try (simpl;reflexivity).
+ assert (Hh := ring_morphism_eq c 0).
+simpl; case_eq (Ceqb c 0);simpl;try reflexivity.
+intros.
+ rewrite Hh. rewrite ring_morphism0.
+ rsimpl. apply Ceqb_eq. trivial. assert (Hh1 := Pcompare_Eq_eq i p);
+destruct (Pos.compare_cont i p Eq).
+ assert (Hh := @Peq_ok P3 P0). case_eq (P3=? P0). intro. simpl.
+ rewrite Hh.
+ rewrite Pphi0. rsimpl. rewrite Pplus_comm. rewrite pow_pos_Pplus;rsimpl.
+rewrite Hh1;trivial. reflexivity. trivial. intros. simpl. reflexivity. simpl. reflexivity.
+ simpl. reflexivity.
+ Qed.
+
+Ltac Esimpl :=
+ repeat (progress (
+ match goal with
+ | |- context [?P@?l] =>
+ match P with
+ | P0 => rewrite (Pphi0 l)
+ | P1 => rewrite (Pphi1 l)
+ | (mkPX ?P ?i ?n ?Q) => rewrite (mkPX_ok l P i n Q)
+ end
+ | |- context [[?c]] =>
+ match c with
+ | 0 => rewrite ring_morphism0
+ | 1 => rewrite ring_morphism1
+ | ?x + ?y => rewrite ring_morphism_add
+ | ?x * ?y => rewrite ring_morphism_mul
+ | ?x - ?y => rewrite ring_morphism_sub
+ | - ?x => rewrite ring_morphism_opp
+ end
+ end));
+ simpl; rsimpl.
+
+ Lemma PaddCl_ok : forall c P l, (PaddCl c P)@l == [c] + P@l .
+ Proof.
+ induction P; simpl; intros; Esimpl; try reflexivity.
+ rewrite IHP2. rsimpl.
+rewrite (ring_add_comm (P2 @ l * pow_pos (nth 0 p l) p0) [c]).
+reflexivity.
+ Qed.
+
+ Lemma PmulC_aux_ok : forall c P l, (PmulC_aux P c)@l == P@l * [c].
+ Proof.
+ induction P;simpl;intros. rewrite ring_morphism_mul.
+try reflexivity.
+ simpl. Esimpl. rewrite IHP1;rewrite IHP2;rsimpl.
+ Qed.
+
+ Lemma PmulC_ok : forall c P l, (PmulC P c)@l == P@l * [c].
+ Proof.
+ intros c P l; unfold PmulC.
+ assert (Hh:= ring_morphism_eq c 0);case_eq (c =? 0). intros.
+ rewrite Hh;Esimpl. apply Ceqb_eq;trivial.
+ assert (H1h:= ring_morphism_eq c 1);case_eq (c =? 1);intros.
+ rewrite H1h;Esimpl. apply Ceqb_eq;trivial.
+ apply PmulC_aux_ok.
+ Qed.
+
+ Lemma Popp_ok : forall P l, (--P)@l == - P@l.
+ Proof.
+ induction P;simpl;intros.
+ Esimpl.
+ rewrite IHP1;rewrite IHP2;rsimpl.
+ Qed.
+
+ Ltac Esimpl2 :=
+ Esimpl;
+ repeat (progress (
+ match goal with
+ | |- context [(PaddCl ?c ?P)@?l] => rewrite (PaddCl_ok c P l)
+ | |- context [(PmulC ?P ?c)@?l] => rewrite (PmulC_ok c P l)
+ | |- context [(--?P)@?l] => rewrite (Popp_ok P l)
+ end)); Esimpl.
+
+Lemma PaddXPX: forall P i n Q,
+ PaddX Padd P i n Q =
+ match Q with
+ | Pc c => mkPX P i n Q
+ | PX P' i' n' Q' =>
+ match Pcompare i i' Eq with
+ | (* i > i' *)
+ Gt => mkPX P i n Q
+ | (* i < i' *)
+ Lt => mkPX P' i' n' (PaddX Padd P i n Q')
+ | (* i = i' *)
+ Eq => match ZPminus n n' with
+ | (* n > n' *)
+ Zpos k => mkPX (PaddX Padd P i k P') i' n' Q'
+ | (* n = n' *)
+ Z0 => mkPX (Padd P P') i n Q'
+ | (* n < n' *)
+ Zneg k => mkPX (Padd P (mkPX P' i k P0)) i n Q'
+ end
+ end
+ end.
+induction Q; reflexivity.
+Qed.
+
+Lemma PaddX_ok2 : forall P2,
+ (forall P l, (P2 ++ P) @ l == P2 @ l + P @ l)
+ /\
+ (forall P k n l,
+ (PaddX Padd P2 k n P) @ l ==
+ P2 @ l * pow_pos (nth 0 k l) n + P @ l).
+induction P2;simpl;intros. split. intros. apply PaddCl_ok.
+ induction P. unfold PaddX. intros. rewrite mkPX_ok.
+ simpl. rsimpl.
+intros. simpl. assert (Hh := Pcompare_Eq_eq k p);
+ destruct (Pos.compare_cont k p Eq).
+ assert (H1h := ZPminus_spec n p0);destruct (ZPminus n p0). Esimpl2.
+rewrite Hh; trivial. rewrite H1h. reflexivity.
+simpl. rewrite mkPX_ok. rewrite IHP1. Esimpl2.
+ rewrite Pplus_comm in H1h.
+rewrite H1h.
+rewrite pow_pos_Pplus. Esimpl2.
+rewrite Hh; trivial. reflexivity.
+rewrite mkPX_ok. rewrite PaddCl_ok. Esimpl2. rewrite Pplus_comm in H1h.
+rewrite H1h. Esimpl2. rewrite pow_pos_Pplus. Esimpl2.
+rewrite Hh; trivial. reflexivity.
+rewrite mkPX_ok. rewrite IHP2. Esimpl2.
+rewrite (ring_add_comm (P2 @ l * pow_pos (nth 0 p l) p0)
+ ([c] * pow_pos (nth 0 k l) n)).
+reflexivity. assert (H1h := ring_morphism_eq c 0);case_eq (Ceqb c 0);
+ intros; simpl.
+rewrite H1h;trivial. Esimpl2. apply Ceqb_eq; trivial. reflexivity.
+decompose [and] IHP2_1. decompose [and] IHP2_2. clear IHP2_1 IHP2_2.
+split. intros. rewrite H0. rewrite H1.
+Esimpl2.
+induction P. unfold PaddX. intros. rewrite mkPX_ok. simpl. reflexivity.
+intros. rewrite PaddXPX.
+assert (H3h := Pcompare_Eq_eq k p1);
+ destruct (Pos.compare_cont k p1 Eq).
+assert (H4h := ZPminus_spec n p2);destruct (ZPminus n p2).
+rewrite mkPX_ok. simpl. rewrite H0. rewrite H1. Esimpl2.
+rewrite H4h. rewrite H3h;trivial. reflexivity.
+rewrite mkPX_ok. rewrite IHP1. Esimpl2. rewrite H3h;trivial.
+rewrite Pplus_comm in H4h.
+rewrite H4h. rewrite pow_pos_Pplus. Esimpl2.
+rewrite mkPX_ok. simpl. rewrite H0. rewrite H1.
+rewrite mkPX_ok.
+ Esimpl2. rewrite H3h;trivial.
+ rewrite Pplus_comm in H4h.
+rewrite H4h. rewrite pow_pos_Pplus. Esimpl2.
+rewrite mkPX_ok. simpl. rewrite IHP2. Esimpl2.
+gen_add_push (P2 @ l * pow_pos (nth 0 p1 l) p2). try reflexivity.
+rewrite mkPX_ok. simpl. reflexivity.
+Qed.
+
+Lemma Padd_ok : forall P Q l, (P ++ Q) @ l == P @ l + Q @ l.
+intro P. elim (PaddX_ok2 P); auto.
+Qed.
+
+Lemma PaddX_ok : forall P2 P k n l,
+ (PaddX Padd P2 k n P) @ l == P2 @ l * pow_pos (nth 0 k l) n + P @ l.
+intro P2. elim (PaddX_ok2 P2); auto.
+Qed.
+
+ Lemma Psub_ok : forall P' P l, (P -- P')@l == P@l - P'@l.
+unfold Psub. intros. rewrite Padd_ok. rewrite Popp_ok. rsimpl.
+ Qed.
+
+ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l.
+induction P'; simpl; intros. rewrite PmulC_ok. reflexivity.
+rewrite PaddX_ok. rewrite IHP'1. rewrite IHP'2. Esimpl2.
+Qed.
+
+ Lemma Psquare_ok : forall P l, (Psquare P)@l == P@l * P@l.
+ Proof.
+ intros. unfold Psquare. apply Pmul_ok.
+ Qed.
+
+ (** Definition of polynomial expressions *)
+
+(*
+ Inductive PExpr : Type :=
+ | PEc : C -> PExpr
+ | PEX : positive -> PExpr
+ | PEadd : PExpr -> PExpr -> PExpr
+ | PEsub : PExpr -> PExpr -> PExpr
+ | PEmul : PExpr -> PExpr -> PExpr
+ | PEopp : PExpr -> PExpr
+ | PEpow : PExpr -> N -> PExpr.
+*)
+
+ (** Specification of the power function *)
+ Section POWER.
+ Variable Cpow : Set.
+ Variable Cp_phi : N -> Cpow.
+ Variable rpow : R -> Cpow -> R.
+
+ Record power_theory : Prop := mkpow_th {
+ rpow_pow_N : forall r n, (rpow r (Cp_phi n))== (pow_N r n)
+ }.
+
+ End POWER.
+ Variable Cpow : Set.
+ Variable Cp_phi : N -> Cpow.
+ Variable rpow : R -> Cpow -> R.
+ Variable pow_th : power_theory Cp_phi rpow.
+
+ (** evaluation of polynomial expressions towards R *)
+ Fixpoint PEeval (l:list R) (pe:PExpr C) {struct pe} : R :=
+ match pe with
+ | PEc c => [c]
+ | PEX j => nth 0 j l
+ | PEadd pe1 pe2 => (PEeval l pe1) + (PEeval l pe2)
+ | PEsub pe1 pe2 => (PEeval l pe1) - (PEeval l pe2)
+ | PEmul pe1 pe2 => (PEeval l pe1) * (PEeval l pe2)
+ | PEopp pe1 => - (PEeval l pe1)
+ | PEpow pe1 n => rpow (PEeval l pe1) (Cp_phi n)
+ end.
+
+Strategy expand [PEeval].
+
+ Definition mk_X j := mkX j.
+
+ (** Correctness proofs *)
+
+ Lemma mkX_ok : forall p l, nth 0 p l == (mk_X p) @ l.
+ Proof.
+ destruct p;simpl;intros;Esimpl;trivial.
+ Qed.
+
+ Ltac Esimpl3 :=
+ repeat match goal with
+ | |- context [(?P1 ++ ?P2)@?l] => rewrite (Padd_ok P1 P2 l)
+ | |- context [(?P1 -- ?P2)@?l] => rewrite (Psub_ok P1 P2 l)
+ end;try Esimpl2;try reflexivity;try apply ring_add_comm.
+
+(* Power using the chinise algorithm *)
+
+Section POWER2.
+ Variable subst_l : Pol -> Pol.
+ Fixpoint Ppow_pos (res P:Pol) (p:positive){struct p} : Pol :=
+ match p with
+ | xH => subst_l (Pmul P res)
+ | xO p => Ppow_pos (Ppow_pos res P p) P p
+ | xI p => subst_l (Pmul P (Ppow_pos (Ppow_pos res P p) P p))
+ end.
+
+ Definition Ppow_N P n :=
+ match n with
+ | N0 => P1
+ | Npos p => Ppow_pos P1 P p
+ end.
+
+ Fixpoint pow_pos_gen (R:Type)(m:R->R->R)(x:R) (i:positive) {struct i}: R :=
+ match i with
+ | xH => x
+ | xO i => let p := pow_pos_gen m x i in m p p
+ | xI i => let p := pow_pos_gen m x i in m x (m p p)
+ end.
+
+Lemma Ppow_pos_ok : forall l, (forall P, subst_l P@l == P@l) ->
+ forall res P p, (Ppow_pos res P p)@l == (pow_pos_gen Pmul P p)@l * res@l.
+ Proof.
+ intros l subst_l_ok res P p. generalize res;clear res.
+ induction p;simpl;intros. try rewrite subst_l_ok.
+ repeat rewrite Pmul_ok. repeat rewrite IHp.
+ rsimpl. repeat rewrite Pmul_ok. repeat rewrite IHp. rsimpl.
+ try rewrite subst_l_ok.
+ repeat rewrite Pmul_ok. reflexivity.
+ Qed.
+
+Definition pow_N_gen (R:Type)(x1:R)(m:R->R->R)(x:R) (p:N) :=
+ match p with
+ | N0 => x1
+ | Npos p => pow_pos_gen m x p
+ end.
+
+ Lemma Ppow_N_ok : forall l, (forall P, subst_l P@l == P@l) ->
+ forall P n, (Ppow_N P n)@l == (pow_N_gen P1 Pmul P n)@l.
+ Proof. destruct n;simpl. reflexivity. rewrite Ppow_pos_ok; trivial. Esimpl. Qed.
+
+ End POWER2.
+
+ (** Normalization and rewriting *)
+
+ Section NORM_SUBST_REC.
+ Let subst_l (P:Pol) := P.
+ Let Pmul_subst P1 P2 := subst_l (Pmul P1 P2).
+ Let Ppow_subst := Ppow_N subst_l.
+
+ Fixpoint norm_aux (pe:PExpr C) : Pol :=
+ match pe with
+ | PEc c => Pc c
+ | PEX j => mk_X j
+ | PEadd pe1 (PEopp pe2) =>
+ Psub (norm_aux pe1) (norm_aux pe2)
+ | PEadd pe1 pe2 => Padd (norm_aux pe1) (norm_aux pe2)
+ | PEsub pe1 pe2 => Psub (norm_aux pe1) (norm_aux pe2)
+ | PEmul pe1 pe2 => Pmul (norm_aux pe1) (norm_aux pe2)
+ | PEopp pe1 => Popp (norm_aux pe1)
+ | PEpow pe1 n => Ppow_N (fun p => p) (norm_aux pe1) n
+ end.
+
+ Definition norm_subst pe := subst_l (norm_aux pe).
+
+
+ Lemma norm_aux_spec :
+ forall l pe,
+ PEeval l pe == (norm_aux pe)@l.
+ Proof.
+ intros.
+ induction pe.
+Esimpl3. Esimpl3. simpl.
+ rewrite IHpe1;rewrite IHpe2.
+ destruct pe2; Esimpl3.
+unfold Psub.
+destruct pe1; destruct pe2; rewrite Padd_ok; rewrite Popp_ok; reflexivity.
+simpl. unfold Psub. rewrite IHpe1;rewrite IHpe2.
+destruct pe1. destruct pe2; rewrite Padd_ok; rewrite Popp_ok; try reflexivity.
+Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3.
+ Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3.
+simpl. rewrite IHpe1;rewrite IHpe2. rewrite Pmul_ok. reflexivity.
+simpl. rewrite IHpe; Esimpl3.
+simpl.
+ rewrite Ppow_N_ok; (intros;try reflexivity).
+ rewrite rpow_pow_N. Esimpl3.
+ induction n;simpl. Esimpl3. induction p; simpl.
+ try rewrite IHp;try rewrite IHpe;
+ repeat rewrite Pms_ok;
+ repeat rewrite Pmul_ok;reflexivity.
+rewrite Pmul_ok. try rewrite IHp;try rewrite IHpe;
+ repeat rewrite Pms_ok;
+ repeat rewrite Pmul_ok;reflexivity. trivial.
+exact pow_th.
+ Qed.
+
+ Lemma norm_subst_spec :
+ forall l pe,
+ PEeval l pe == (norm_subst pe)@l.
+ Proof.
+ intros;unfold norm_subst.
+ unfold subst_l. apply norm_aux_spec.
+ Qed.
+
+ End NORM_SUBST_REC.
+
+ Fixpoint interp_PElist (l:list R) (lpe:list (PExpr C * PExpr C)) {struct lpe} : Prop :=
+ match lpe with
+ | nil => True
+ | (me,pe)::lpe =>
+ match lpe with
+ | nil => PEeval l me == PEeval l pe
+ | _ => PEeval l me == PEeval l pe /\ interp_PElist l lpe
+ end
+ end.
+
+
+ Lemma norm_subst_ok : forall l pe,
+ PEeval l pe == (norm_subst pe)@l.
+ Proof.
+ intros;apply norm_subst_spec.
+ Qed.
+
+
+ Lemma ring_correct : forall l pe1 pe2,
+ (norm_subst pe1 =? norm_subst pe2) = true ->
+ PEeval l pe1 == PEeval l pe2.
+ Proof.
+ simpl;intros.
+ do 2 (rewrite (norm_subst_ok l);trivial).
+ apply Peq_ok;trivial.
+ Qed.
+
+End MakeRingPol.
diff --git a/plugins/setoid_ring/Ncring_tac.v b/plugins/setoid_ring/Ncring_tac.v
new file mode 100644
index 00000000..34731eb3
--- /dev/null
+++ b/plugins/setoid_ring/Ncring_tac.v
@@ -0,0 +1,308 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* constr:(t1::t2::nil)
+ | ?t1 = ?t2 => constr:(t1::t2::nil)
+ | (_ ?t1 ?t2) => constr:(t1::t2::nil)
+ end.
+
+Lemma Zeqb_ok: forall x y : Z, Zeq_bool x y = true -> x == y.
+ intros x y H. rewrite (Zeq_bool_eq x y H). reflexivity. Qed.
+
+Ltac reify_goal lvar lexpr lterm:=
+ (*idtac lvar; idtac lexpr; idtac lterm;*)
+ match lexpr with
+ nil => idtac
+ | ?e1::?e2::_ =>
+ match goal with
+ |- (?op ?u1 ?u2) =>
+ change (op
+ (@PEeval Z _ _ _ _ _ _ _ _ _ (@gen_phiZ _ _ _ _ _ _ _ _ _) N
+ (fun n:N => n) (@pow_N _ _ _ _ _ _ _ _ _)
+ lvar e1)
+ (@PEeval Z _ _ _ _ _ _ _ _ _ (@gen_phiZ _ _ _ _ _ _ _ _ _) N
+ (fun n:N => n) (@pow_N _ _ _ _ _ _ _ _ _)
+ lvar e2))
+ end
+ end.
+
+Lemma comm: forall (R:Type)`{Ring R}(c : Z) (x : R),
+ x * (gen_phiZ c) == (gen_phiZ c) * x.
+induction c. intros. simpl. gen_rewrite. simpl. intros.
+rewrite <- same_gen.
+induction p. simpl. gen_rewrite. rewrite IHp. reflexivity.
+simpl. gen_rewrite. rewrite IHp. reflexivity.
+simpl. gen_rewrite.
+simpl. intros. rewrite <- same_gen.
+induction p. simpl. generalize IHp. clear IHp.
+gen_rewrite. intro IHp. rewrite IHp. reflexivity.
+simpl. generalize IHp. clear IHp.
+gen_rewrite. intro IHp. rewrite IHp. reflexivity.
+simpl. gen_rewrite. Qed.
+
+Ltac ring_gen :=
+ match goal with
+ |- ?g => let lterm := lterm_goal g in
+ match eval red in (list_reifyl (lterm:=lterm)) with
+ | (?fv, ?lexpr) =>
+ (*idtac "variables:";idtac fv;
+ idtac "terms:"; idtac lterm;
+ idtac "reifications:"; idtac lexpr; *)
+ reify_goal fv lexpr lterm;
+ match goal with
+ |- ?g =>
+ apply (@ring_correct Z _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
+ (@gen_phiZ _ _ _ _ _ _ _ _ _) _
+ (@comm _ _ _ _ _ _ _ _ _ _) Zeq_bool Zeqb_ok N (fun n:N => n)
+ (@pow_N _ _ _ _ _ _ _ _ _));
+ [apply mkpow_th; reflexivity
+ |vm_compute; reflexivity]
+ end
+ end
+ end.
+
+Ltac non_commutative_ring:=
+ intros;
+ ring_gen.
+
+(* simplification *)
+
+Ltac ring_simplify_aux lterm fv lexpr hyp :=
+ match lterm with
+ | ?t0::?lterm =>
+ match lexpr with
+ | ?e::?le => (* e:PExpr Z est la réification de t0:R *)
+ let t := constr:(@Ncring_polynom.norm_subst
+ Z 0%Z 1%Z Zplus Zmult Zminus Zopp (@eq Z) Zops Zeq_bool e) in
+ (* t:Pol Z *)
+ let te :=
+ constr:(@Ncring_polynom.Pphi Z
+ _ 0 1 _+_ _*_ _-_ -_ _==_ _ Ncring_initial.gen_phiZ fv t) in
+ let eq1 := fresh "ring" in
+ let nft := eval vm_compute in t in
+ let t':= fresh "t" in
+ pose (t' := nft);
+ assert (eq1 : t = t');
+ [vm_cast_no_check (refl_equal t')|
+ let eq2 := fresh "ring" in
+ assert (eq2:(@Ncring_polynom.PEeval Z
+ _ 0 1 _+_ _*_ _-_ -_ _==_ _ Ncring_initial.gen_phiZ N (fun n:N => n)
+ (@Ring_theory.pow_N _ 1 multiplication) fv e) == te);
+ [apply (@Ncring_polynom.norm_subst_ok
+ Z _ 0%Z 1%Z Zplus Zmult Zminus Zopp (@eq Z)
+ _ _ 0 1 _+_ _*_ _-_ -_ _==_ _ _ Ncring_initial.gen_phiZ _
+ (@comm _ 0 1 _+_ _*_ _-_ -_ _==_ _ _) _ Zeqb_ok);
+ apply mkpow_th; reflexivity
+ | match hyp with
+ | 1%nat => rewrite eq2
+ | ?H => try rewrite eq2 in H
+ end];
+ let P:= fresh "P" in
+ match hyp with
+ | 1%nat => idtac "ok";
+ rewrite eq1;
+ pattern (@Ncring_polynom.Pphi Z _ 0 1 _+_ _*_ _-_ -_ _==_
+ _ Ncring_initial.gen_phiZ fv t');
+ match goal with
+ |- (?p ?t) => set (P:=p)
+ end;
+ unfold t' in *; clear t' eq1 eq2; simpl
+ | ?H =>
+ rewrite eq1 in H;
+ pattern (@Ncring_polynom.Pphi Z _ 0 1 _+_ _*_ _-_ -_ _==_
+ _ Ncring_initial.gen_phiZ fv t') in H;
+ match type of H with
+ | (?p ?t) => set (P:=p) in H
+ end;
+ unfold t' in *; clear t' eq1 eq2; simpl in H
+ end; unfold P in *; clear P
+ ]; ring_simplify_aux lterm fv le hyp
+ | nil => idtac
+ end
+ | nil => idtac
+ end.
+
+Ltac set_variables fv :=
+ match fv with
+ | nil => idtac
+ | ?t::?fv =>
+ let v := fresh "X" in
+ set (v:=t) in *; set_variables fv
+ end.
+
+Ltac deset n:=
+ match n with
+ | 0%nat => idtac
+ | S ?n1 =>
+ match goal with
+ | h:= ?v : ?t |- ?g => unfold h in *; clear h; deset n1
+ end
+ end.
+
+(* a est soit un terme de l'anneau, soit une liste de termes.
+J'ai pas réussi à un décomposer les Vlists obtenues avec ne_constr_list
+ dans Tactic Notation *)
+
+Ltac ring_simplify_gen a hyp :=
+ let lterm :=
+ match a with
+ | _::_ => a
+ | _ => constr:(a::nil)
+ end in
+ match eval red in (list_reifyl (lterm:=lterm)) with
+ | (?fv, ?lexpr) => idtac lterm; idtac fv; idtac lexpr;
+ let n := eval compute in (length fv) in
+ idtac n;
+ let lt:=fresh "lt" in
+ set (lt:= lterm);
+ let lv:=fresh "fv" in
+ set (lv:= fv);
+ (* les termes de fv sont remplacés par des variables
+ pour pouvoir utiliser simpl ensuite sans risquer
+ des simplifications indésirables *)
+ set_variables fv;
+ let lterm1 := eval unfold lt in lt in
+ let lv1 := eval unfold lv in lv in
+ idtac lterm1; idtac lv1;
+ ring_simplify_aux lterm1 lv1 lexpr hyp;
+ clear lt lv;
+ (* on remet les termes de fv *)
+ deset n
+ end.
+
+Tactic Notation "non_commutative_ring_simplify" constr(lterm):=
+ ring_simplify_gen lterm 1%nat.
+
+Tactic Notation "non_commutative_ring_simplify" constr(lterm) "in" ident(H):=
+ ring_simplify_gen lterm H.
+
+
diff --git a/plugins/setoid_ring/Ring.v b/plugins/setoid_ring/Ring.v
index 7b48f590..c44c2edf 100644
--- a/plugins/setoid_ring/Ring.v
+++ b/plugins/setoid_ring/Ring.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* Cpow.
Variable rpow : R -> Cpow -> R.
Variable pow_th : power_theory rI rmul req Cp_phi rpow.
@@ -104,12 +104,12 @@ Section MakeRingPol.
match P, P' with
| Pc c, Pc c' => c ?=! c'
| Pinj j Q, Pinj j' Q' =>
- match Pcompare j j' Eq with
+ match j ?= j' with
| Eq => Peq Q Q'
| _ => false
end
| PX P i Q, PX P' i' Q' =>
- match Pcompare i i' Eq with
+ match i ?= i' with
| Eq => if Peq P P' then Peq Q Q' else false
| _ => false
end
@@ -435,7 +435,7 @@ Section MakeRingPol.
CFactor P c
| Pc _, _ => (P, Pc cO)
| Pinj j1 P1, zmon j2 M1 =>
- match (j1 ?= j2) Eq with
+ match j1 ?= j2 with
Eq => let (R,S) := MFactor P1 c M1 in
(mkPinj j1 R, mkPinj j1 S)
| Lt => let (R,S) := MFactor P1 c (zmon (j2 - j1) M1) in
@@ -449,7 +449,7 @@ Section MakeRingPol.
let (R2, S2) := MFactor Q1 c M2 in
(mkPX R1 i R2, mkPX S1 i S2)
| PX P1 i Q1, vmon j M1 =>
- match (i ?= j) Eq with
+ match i ?= j with
Eq => let (R1,S1) := MFactor P1 c (mkZmon xH M1) in
(mkPX R1 i Q1, S1)
| Lt => let (R1,S1) := MFactor P1 c (vmon (j - i) M1) in
@@ -552,10 +552,10 @@ Section MakeRingPol.
Proof.
induction P;destruct P';simpl;intros;try discriminate;trivial.
apply (morph_eq CRmorph);trivial.
- assert (H1 := Pcompare_Eq_eq p p0); destruct ((p ?= p0)%positive Eq);
+ assert (H1 := Pos.compare_eq p p0); destruct (p ?= p0);
try discriminate H.
rewrite (IHP P' H); rewrite H1;trivial;rrefl.
- assert (H1 := Pcompare_Eq_eq p p0); destruct ((p ?= p0)%positive Eq);
+ assert (H1 := Pos.compare_eq p p0); destruct (p ?= p0);
try discriminate H.
rewrite H1;trivial. clear H1.
assert (H1 := IHP1 P'1);assert (H2 := IHP2 P'2);
@@ -947,8 +947,8 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l.
generalize (Mcphi_ok P c (jump i l)); case CFactor.
intros R1 Q1 HH; rewrite HH; Esimpl.
intros j M.
- case_eq ((i ?= j) Eq); intros He; simpl.
- rewrite (Pcompare_Eq_eq _ _ He).
+ case_eq (i ?= j); intros He; simpl.
+ rewrite (Pos.compare_eq _ _ He).
generalize (Hrec (c, M) (jump j l)); case (MFactor P c M);
simpl; intros P2 Q2 H; repeat rewrite mkPinj_ok; auto.
generalize (Hrec (c, (zmon (j -i) M)) (jump i l));
@@ -987,8 +987,8 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l.
rewrite (ARadd_comm ARth); rsimpl.
rewrite zmon_pred_ok;rsimpl.
intros j M1.
- case_eq ((i ?= j) Eq); intros He; simpl.
- rewrite (Pcompare_Eq_eq _ _ He).
+ case_eq (i ?= j); intros He; simpl.
+ rewrite (Pos.compare_eq _ _ He).
generalize (Hrec1 (c, mkZmon xH M1) l); case (MFactor P2 c (mkZmon xH M1));
simpl; intros P3 Q3 H; repeat rewrite mkPinj_ok; auto.
rewrite H; rewrite mkPX_ok; rsimpl.
diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v
index 4fbdcbaa..ab992552 100644
--- a/plugins/setoid_ring/Ring_theory.v
+++ b/plugins/setoid_ring/Ring_theory.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* Cpow.
Variable rpow : R -> Cpow -> R.
@@ -590,6 +590,21 @@ Ltac gen_srewrite Rsth Reqe ARth :=
| progress rewrite <- (ARopp_mul_l ARth)
| progress rewrite <- (ARopp_mul_r Rsth Reqe ARth) ].
+Ltac gen_srewrite_sr Rsth Reqe ARth :=
+ repeat first
+ [ gen_reflexivity Rsth
+ | progress rewrite (ARopp_zero Rsth Reqe ARth)
+ | rewrite (ARadd_0_l ARth)
+ | rewrite (ARadd_0_r Rsth ARth)
+ | rewrite (ARmul_1_l ARth)
+ | rewrite (ARmul_1_r Rsth ARth)
+ | rewrite (ARmul_0_l ARth)
+ | rewrite (ARmul_0_r Rsth ARth)
+ | rewrite (ARdistr_l ARth)
+ | rewrite (ARdistr_r Rsth Reqe ARth)
+ | rewrite (ARadd_assoc ARth)
+ | rewrite (ARmul_assoc ARth) ].
+
Ltac gen_add_push add Rsth Reqe ARth x :=
repeat (match goal with
| |- context [add (add ?y x) ?z] =>
diff --git a/plugins/setoid_ring/Rings_Q.v b/plugins/setoid_ring/Rings_Q.v
new file mode 100644
index 00000000..fd765471
--- /dev/null
+++ b/plugins/setoid_ring/Rings_Q.v
@@ -0,0 +1,30 @@
+Require Export Cring.
+Require Export Integral_domain.
+
+(* Rational numbers *)
+Require Import QArith.
+
+Instance Qops: (@Ring_ops Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq).
+
+Instance Qri : (Ring (Ro:=Qops)).
+constructor.
+try apply Q_Setoid.
+apply Qplus_comp.
+apply Qmult_comp.
+apply Qminus_comp.
+apply Qopp_comp.
+ exact Qplus_0_l. exact Qplus_comm. apply Qplus_assoc.
+ exact Qmult_1_l. exact Qmult_1_r. apply Qmult_assoc.
+ apply Qmult_plus_distr_l. intros. apply Qmult_plus_distr_r.
+reflexivity. exact Qplus_opp_r.
+Defined.
+
+Instance Qcri: (Cring (Rr:=Qri)).
+red. exact Qmult_comm. Defined.
+
+Lemma Q_one_zero: not (Qeq 1%Q 0%Q).
+unfold Qeq. simpl. auto with *. Qed.
+
+Instance Qdi : (Integral_domain (Rcr:=Qcri)).
+constructor.
+exact Qmult_integral. exact Q_one_zero. Defined.
diff --git a/plugins/setoid_ring/Rings_R.v b/plugins/setoid_ring/Rings_R.v
new file mode 100644
index 00000000..fd219c23
--- /dev/null
+++ b/plugins/setoid_ring/Rings_R.v
@@ -0,0 +1,34 @@
+Require Export Cring.
+Require Export Integral_domain.
+
+(* Real numbers *)
+Require Import Reals.
+Require Import RealField.
+
+Lemma Rsth : Setoid_Theory R (@eq R).
+constructor;red;intros;subst;trivial.
+Qed.
+
+Instance Rops: (@Ring_ops R 0%R 1%R Rplus Rmult Rminus Ropp (@eq R)).
+
+Instance Rri : (Ring (Ro:=Rops)).
+constructor;
+try (try apply Rsth;
+ try (unfold respectful, Proper; unfold equality; unfold eq_notation in *;
+ intros; try rewrite H; try rewrite H0; reflexivity)).
+ exact Rplus_0_l. exact Rplus_comm. symmetry. apply Rplus_assoc.
+ exact Rmult_1_l. exact Rmult_1_r. symmetry. apply Rmult_assoc.
+ exact Rmult_plus_distr_r. intros; apply Rmult_plus_distr_l.
+exact Rplus_opp_r.
+Defined.
+
+Instance Rcri: (Cring (Rr:=Rri)).
+red. exact Rmult_comm. Defined.
+
+Lemma R_one_zero: 1%R <> 0%R.
+discrR.
+Qed.
+
+Instance Rdi : (Integral_domain (Rcr:=Rcri)).
+constructor.
+exact Rmult_integral. exact R_one_zero. Defined.
diff --git a/plugins/setoid_ring/Rings_Z.v b/plugins/setoid_ring/Rings_Z.v
new file mode 100644
index 00000000..88904865
--- /dev/null
+++ b/plugins/setoid_ring/Rings_Z.v
@@ -0,0 +1,14 @@
+Require Export Cring.
+Require Export Integral_domain.
+Require Export Ncring_initial.
+
+Instance Zcri: (Cring (Rr:=Zr)).
+red. exact Zmult_comm. Defined.
+
+Lemma Z_one_zero: 1%Z <> 0%Z.
+omega.
+Qed.
+
+Instance Zdi : (Integral_domain (Rcr:=Zcri)).
+constructor.
+exact Zmult_integral. exact Z_one_zero. Defined.
diff --git a/plugins/setoid_ring/ZArithRing.v b/plugins/setoid_ring/ZArithRing.v
index 362542b9..d3ed36ee 100644
--- a/plugins/setoid_ring/ZArithRing.v
+++ b/plugins/setoid_ring/ZArithRing.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* constr:false
end.
-Definition N_of_Z x :=
- match x with
- | Zpos p => Npos p
- | _ => N0
- end.
+Notation N_of_Z := Z.to_N (only parsing).
Ltac Zpow_tac t :=
match isZpow_coef t with
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 820246af..9d61c06d 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* None
let interp_map l t =
- try Some(List.assoc t l) with Not_found -> None
+ try Some(list_assoc_f eq_constr t l) with Not_found -> None
let protect_maps = ref Stringmap.empty
let add_map s m = protect_maps := Stringmap.add s m !protect_maps
@@ -98,13 +95,13 @@ let lookup_map map =
let protect_red map env sigma c =
kl (create_clos_infos betadeltaiota env)
- (mk_clos_but (lookup_map map c) (Esubst.ESID 0) c);;
+ (mk_clos_but (lookup_map map c) (Esubst.subs_id 0) c);;
let protect_tac map =
Tactics.reduct_option (protect_red map,DEFAULTcast) None ;;
let protect_tac_in map id =
- Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id,InHyp));;
+ Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id, Termops.InHyp));;
TACTIC EXTEND protect_fv
@@ -144,7 +141,7 @@ let closed_term_ast l =
let l = List.map (fun gr -> ArgArg(dummy_loc,gr)) l in
TacFun([Some(id_of_string"t")],
TacAtom(dummy_loc,TacExtend(dummy_loc,"closed_term",
- [Genarg.in_gen Genarg.globwit_constr (RVar(dummy_loc,id_of_string"t"),None);
+ [Genarg.in_gen Genarg.globwit_constr (GVar(dummy_loc,id_of_string"t"),None);
Genarg.in_gen (Genarg.wit_list1 Genarg.globwit_ref) l])))
(*
let _ = add_tacdef false ((dummy_loc,id_of_string"ring_closed_term"
@@ -161,18 +158,18 @@ let ty c = Typing.type_of (Global.env()) Evd.empty c
let decl_constant na c =
mkConst(declare_constant (id_of_string na) (DefinitionEntry
{ const_entry_body = c;
+ const_entry_secctx = None;
const_entry_type = None;
- const_entry_opaque = true;
- const_entry_boxed = true},
+ const_entry_opaque = true },
IsProof Lemma))
(* Calling a global tactic *)
let ltac_call tac (args:glob_tactic_arg list) =
- TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force tac),args))
+ TacArg(dummy_loc,TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force tac),args))
(* Calling a locally bound tactic *)
let ltac_lcall tac args =
- TacArg(TacCall(dummy_loc, ArgVar(dummy_loc, id_of_string tac),args))
+ TacArg(dummy_loc,TacCall(dummy_loc, ArgVar(dummy_loc, id_of_string tac),args))
let ltac_letin (x, e1) e2 =
TacLetIn(false,[(dummy_loc,id_of_string x),e1],e2)
@@ -188,8 +185,10 @@ let ltac_record flds =
let carg c = TacDynamic(dummy_loc,Pretyping.constr_in c)
let dummy_goal env =
- {Evd.it = Evd.make_evar (named_context_val env) mkProp;
- Evd.sigma = Evd.empty}
+ let (gl,_,sigma) =
+ Goal.V82.mk_goal Evd.empty (named_context_val env) mkProp Store.empty in
+ {Evd.it = gl;
+ Evd.sigma = sigma}
let exec_tactic env n f args =
let lid = list_tabulate(fun i -> id_of_string("x"^string_of_int i)) n in
@@ -344,7 +343,7 @@ type ring_info =
ring_pre_tac : glob_tactic_expr;
ring_post_tac : glob_tactic_expr }
-module Cmap = Map.Make(struct type t = constr let compare = compare end)
+module Cmap = Map.Make(struct type t = constr let compare = constr_ord end)
let from_carrier = ref Cmap.empty
let from_relation = ref Cmap.empty
@@ -415,7 +414,7 @@ let subst_th (subst,th) =
let posttac'= subst_tactic subst th.ring_post_tac in
if c' == th.ring_carrier &&
eq' == th.ring_req &&
- set' = th.ring_setoid &&
+ eq_constr set' th.ring_setoid &&
ext' == th.ring_ext &&
morph' == th.ring_morph &&
th' == th.ring_th &&
@@ -440,7 +439,7 @@ let subst_th (subst,th) =
ring_post_tac = posttac' }
-let (theory_to_obj, obj_to_theory) =
+let theory_to_obj : ring_info -> obj =
let cache_th (name,th) = add_entry name th in
declare_object
{(default_object "tactic-new-ring-theory") with
@@ -576,13 +575,13 @@ let dest_ring env sigma th_spec =
let th_typ = Retyping.get_type_of env sigma th_spec in
match kind_of_term th_typ with
App(f,[|r;zero;one;add;mul;sub;opp;req|])
- when f = Lazy.force coq_almost_ring_theory ->
+ when eq_constr f (Lazy.force coq_almost_ring_theory) ->
(None,r,zero,one,add,mul,Some sub,Some opp,req)
| App(f,[|r;zero;one;add;mul;req|])
- when f = Lazy.force coq_semi_ring_theory ->
+ when eq_constr f (Lazy.force coq_semi_ring_theory) ->
(Some true,r,zero,one,add,mul,None,None,req)
| App(f,[|r;zero;one;add;mul;sub;opp;req|])
- when f = Lazy.force coq_ring_theory ->
+ when eq_constr f (Lazy.force coq_ring_theory) ->
(Some false,r,zero,one,add,mul,Some sub,Some opp,req)
| _ -> error "bad ring structure"
@@ -592,10 +591,10 @@ let dest_morph env sigma m_spec =
match kind_of_term m_typ with
App(f,[|r;zero;one;add;mul;sub;opp;req;
c;czero;cone;cadd;cmul;csub;copp;ceqb;phi|])
- when f = Lazy.force coq_ring_morph ->
+ when eq_constr f (Lazy.force coq_ring_morph) ->
(c,czero,cone,cadd,cmul,Some csub,Some copp,ceqb,phi)
| App(f,[|r;zero;one;add;mul;req;c;czero;cone;cadd;cmul;ceqb;phi|])
- when f = Lazy.force coq_semi_morph ->
+ when eq_constr f (Lazy.force coq_semi_morph) ->
(c,czero,cone,cadd,cmul,None,None,ceqb,phi)
| _ -> error "bad morphism structure"
@@ -626,23 +625,23 @@ let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac =
(match rk, opp, kind with
Abstract, None, _ ->
let t = ArgArg(dummy_loc,Lazy.force ltac_inv_morphN) in
- TacArg(TacCall(dummy_loc,t,List.map carg [zero;one;add;mul]))
+ TacArg(dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;add;mul]))
| Abstract, Some opp, Some _ ->
let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morphZ) in
- TacArg(TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp]))
+ TacArg(dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp]))
| Abstract, Some opp, None ->
let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morphNword) in
TacArg
- (TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp]))
+ (dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp]))
| Computational _,_,_ ->
let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_gen) in
TacArg
- (TacCall(dummy_loc,t,List.map carg [zero;one;zero;one]))
+ (dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;zero;one]))
| Morphism mth,_,_ ->
let (_,czero,cone,_,_,_,_,_,_) = dest_morph env sigma mth in
let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_gen) in
TacArg
- (TacCall(dummy_loc,t,List.map carg [zero;one;czero;cone])))
+ (dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;czero;cone])))
let make_hyp env c =
let t = Retyping.get_type_of env Evd.empty c in
@@ -659,7 +658,7 @@ let interp_power env pow =
match pow with
| None ->
let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_nothing) in
- (TacArg(TacCall(dummy_loc,t,[])), lapp coq_None [|carrier|])
+ (TacArg(dummy_loc,TacCall(dummy_loc,t,[])), lapp coq_None [|carrier|])
| Some (tac, spec) ->
let tac =
match tac with
@@ -832,7 +831,7 @@ let ring_lookup (f:glob_tactic_expr) lH rl t gl =
TACTIC EXTEND ring_lookup
| [ "ring_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lrt) ] ->
- [ let (t,lr) = list_sep_last lrt in ring_lookup (fst f) lH lr t]
+ [ let (t,lr) = list_sep_last lrt in ring_lookup f lH lr t]
END
@@ -893,18 +892,18 @@ let dest_field env sigma th_spec =
let th_typ = Retyping.get_type_of env sigma th_spec in
match kind_of_term th_typ with
| App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|])
- when f = Lazy.force afield_theory ->
+ when eq_constr f (Lazy.force afield_theory) ->
let rth = lapp af_ar
[|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in
(None,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth)
| App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|])
- when f = Lazy.force field_theory ->
+ when eq_constr f (Lazy.force field_theory) ->
let rth =
lapp f_r
[|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in
(Some false,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth)
| App(f,[|r;zero;one;add;mul;div;inv;req|])
- when f = Lazy.force sfield_theory ->
+ when eq_constr f (Lazy.force sfield_theory) ->
let rth = lapp sf_sr
[|r;zero;one;add;mul;div;inv;req;th_spec|] in
(Some true,r,zero,one,add,mul,None,None,div,inv,req,rth)
@@ -1016,7 +1015,7 @@ let subst_th (subst,th) =
field_pre_tac = pretac';
field_post_tac = posttac' }
-let (ftheory_to_obj, obj_to_ftheory) =
+let ftheory_to_obj : field_info -> obj =
let cache_th (name,th) = add_field_entry name th in
declare_object
{(default_object "tactic-new-field-theory") with
@@ -1160,5 +1159,5 @@ let field_lookup (f:glob_tactic_expr) lH rl t gl =
TACTIC EXTEND field_lookup
| [ "field_lookup" tactic(f) "[" constr_list(lH) "]" ne_constr_list(lt) ] ->
- [ let (t,l) = list_sep_last lt in field_lookup (fst f) lH l t ]
+ [ let (t,l) = list_sep_last lt in field_lookup f lH l t ]
END
diff --git a/plugins/setoid_ring/vo.itarget b/plugins/setoid_ring/vo.itarget
index 6934375b..580df9b5 100644
--- a/plugins/setoid_ring/vo.itarget
+++ b/plugins/setoid_ring/vo.itarget
@@ -13,3 +13,13 @@ Ring_tac.vo
Ring_theory.vo
Ring.vo
ZArithRing.vo
+Algebra_syntax.vo
+Cring.vo
+Ncring.vo
+Ncring_polynom.vo
+Ncring_initial.vo
+Ncring_tac.vo
+Rings_Z.vo
+Rings_R.vo
+Rings_Q.vo
+Integral_domain.vo
\ No newline at end of file
--
cgit v1.2.3
From e0d682ec25282a348d35c5b169abafec48555690 Mon Sep 17 00:00:00 2001
From: Stephane Glondu
Date: Mon, 20 Aug 2012 18:27:01 +0200
Subject: Imported Upstream version 8.4dfsg
---
.gitignore | 5 +-
CHANGES | 166 +-
COMPATIBILITY | 47 +-
INSTALL | 2 +-
INSTALL.macosx | 20 -
Makefile | 36 +-
Makefile.build | 33 +-
Makefile.common | 23 +-
TODO | 53 +
checker/check.ml | 2 +-
checker/check_stat.ml | 2 +-
checker/check_stat.mli | 2 +-
checker/checker.ml | 2 +-
checker/closure.ml | 2 +-
checker/closure.mli | 2 +-
checker/indtypes.ml | 2 +-
checker/indtypes.mli | 2 +-
checker/inductive.ml | 2 +-
checker/inductive.mli | 2 +-
checker/mod_checking.mli | 2 +-
checker/modops.ml | 2 +-
checker/modops.mli | 2 +-
checker/reduction.ml | 2 +-
checker/reduction.mli | 2 +-
checker/safe_typing.ml | 2 +-
checker/safe_typing.mli | 2 +-
checker/subtyping.ml | 2 +-
checker/subtyping.mli | 2 +-
checker/term.ml | 2 +-
checker/type_errors.ml | 2 +-
checker/type_errors.mli | 2 +-
checker/typeops.ml | 2 +-
checker/typeops.mli | 2 +-
checker/validate.ml | 2 +-
config/Makefile.template | 154 --
config/coq_config.mli | 2 +-
configure | 478 ++---
dev/db_printers.ml | 2 +-
dev/header | 2 +-
dev/macosify_accel.sh | 3 +
dev/top_printers.ml | 4 +-
doc/refman/RefMan-sch.tex | 418 -----
doc/stdlib/index-list.html.template | 6 +
ide/command_windows.ml | 2 +-
ide/command_windows.mli | 2 +-
ide/config_lexer.mll | 2 +-
ide/coq.ml | 2 +-
ide/coq.mli | 2 +-
ide/coq_commands.ml | 2 +-
ide/coq_lex.mll | 2 +-
ide/coqide.ml | 13 +-
ide/coqide.mli | 2 +-
ide/coqide_main.ml4 | 2 +-
ide/gtk_parsing.ml | 2 +-
ide/ide_mac_stubs.c | 10 +-
ide/ideproof.ml | 40 +-
ide/ideutils.ml | 2 +-
ide/ideutils.mli | 2 +-
ide/mac_default_accel_map | 726 ++++----
ide/minilib.ml | 55 +-
ide/preferences.ml | 4 +-
ide/preferences.mli | 2 +-
ide/project_file.ml4 | 2 +-
ide/tags.ml | 2 +-
ide/tags.mli | 2 +-
ide/typed_notebook.ml | 2 +-
ide/undo.ml | 2 +-
ide/undo_lablgtk_ge212.mli | 2 +-
ide/undo_lablgtk_ge26.mli | 2 +-
ide/undo_lablgtk_lt26.mli | 2 +-
ide/utf8_convert.mll | 2 +-
interp/constrextern.ml | 58 +-
interp/constrextern.mli | 4 +-
interp/constrintern.ml | 31 +-
interp/constrintern.mli | 2 +-
interp/coqlib.ml | 2 +-
interp/coqlib.mli | 2 +-
interp/dumpglob.ml | 2 +-
interp/dumpglob.mli | 2 +-
interp/genarg.ml | 2 +-
interp/genarg.mli | 2 +-
interp/implicit_quantifiers.ml | 2 +-
interp/implicit_quantifiers.mli | 2 +-
interp/modintern.ml | 2 +-
interp/modintern.mli | 2 +-
interp/notation.ml | 35 +-
interp/notation.mli | 2 +-
interp/ppextend.ml | 2 +-
interp/ppextend.mli | 2 +-
interp/reserve.ml | 2 +-
interp/reserve.mli | 2 +-
interp/smartlocate.ml | 2 +-
interp/smartlocate.mli | 2 +-
interp/syntax_def.ml | 66 +-
interp/syntax_def.mli | 12 +-
interp/topconstr.ml | 2 +-
interp/topconstr.mli | 2 +-
kernel/cbytecodes.ml | 2 +-
kernel/cbytecodes.mli | 4 +-
kernel/cbytegen.ml | 2 +-
kernel/cemitcodes.ml | 2 +-
kernel/closure.ml | 2 +-
kernel/closure.mli | 2 +-
kernel/conv_oracle.ml | 2 +-
kernel/conv_oracle.mli | 2 +-
kernel/cooking.ml | 8 +-
kernel/cooking.mli | 5 +-
kernel/csymtable.ml | 2 +-
kernel/csymtable.mli | 4 +-
kernel/declarations.ml | 2 +-
kernel/declarations.mli | 2 +-
kernel/entries.ml | 2 +-
kernel/entries.mli | 2 +-
kernel/environ.ml | 2 +-
kernel/environ.mli | 2 +-
kernel/esubst.ml | 2 +-
kernel/esubst.mli | 2 +-
kernel/indtypes.ml | 2 +-
kernel/indtypes.mli | 2 +-
kernel/inductive.ml | 2 +-
kernel/inductive.mli | 2 +-
kernel/mod_subst.ml | 2 +-
kernel/mod_subst.mli | 2 +-
kernel/mod_typing.ml | 2 +-
kernel/mod_typing.mli | 2 +-
kernel/modops.ml | 2 +-
kernel/modops.mli | 2 +-
kernel/names.ml | 2 +-
kernel/names.mli | 2 +-
kernel/pre_env.ml | 2 +-
kernel/pre_env.mli | 2 +-
kernel/reduction.ml | 2 +-
kernel/reduction.mli | 2 +-
kernel/retroknowledge.ml | 2 +-
kernel/retroknowledge.mli | 2 +-
kernel/safe_typing.ml | 2 +-
kernel/safe_typing.mli | 2 +-
kernel/sign.ml | 2 +-
kernel/sign.mli | 2 +-
kernel/subtyping.ml | 2 +-
kernel/subtyping.mli | 2 +-
kernel/term.ml | 3 +-
kernel/term.mli | 3 +-
kernel/term_typing.ml | 5 +-
kernel/term_typing.mli | 2 +-
kernel/type_errors.ml | 2 +-
kernel/type_errors.mli | 2 +-
kernel/typeops.ml | 2 +-
kernel/typeops.mli | 2 +-
kernel/univ.ml | 2 +-
kernel/univ.mli | 2 +-
kernel/vconv.mli | 2 +-
kernel/vm.ml | 2 +-
lib/bigint.ml | 355 ++--
lib/bigint.mli | 11 +-
lib/compat.ml4 | 2 +-
lib/dnet.ml | 2 +-
lib/dnet.mli | 2 +-
lib/dyn.ml | 2 +-
lib/dyn.mli | 2 +-
lib/envars.ml | 10 +-
lib/envars.mli | 2 +-
lib/explore.ml | 2 +-
lib/explore.mli | 2 +-
lib/flags.ml | 17 +-
lib/flags.mli | 7 +-
lib/gmap.ml | 2 +-
lib/gmap.mli | 2 +-
lib/gmapl.ml | 2 +-
lib/gmapl.mli | 2 +-
lib/hashcons.ml | 2 +-
lib/hashcons.mli | 2 +-
lib/hashtbl_alt.ml | 2 +-
lib/hashtbl_alt.mli | 2 +-
lib/heap.ml | 2 +-
lib/heap.mli | 2 +-
lib/option.ml | 2 +-
lib/option.mli | 2 +-
lib/pp.ml4 | 13 +-
lib/pp.mli | 6 +-
lib/pp_control.ml | 2 +-
lib/pp_control.mli | 2 +-
lib/profile.ml | 2 +-
lib/profile.mli | 2 +-
lib/rtree.ml | 2 +-
lib/rtree.mli | 2 +-
lib/system.ml | 2 +-
lib/system.mli | 2 +-
lib/tries.ml | 2 +-
lib/unionfind.ml | 2 +-
lib/unionfind.mli | 2 +-
lib/util.mli | 2 +-
lib/xml_lexer.mll | 6 +
library/assumptions.ml | 2 +-
library/assumptions.mli | 2 +-
library/decl_kinds.ml | 2 +-
library/decl_kinds.mli | 2 +-
library/declare.ml | 2 +-
library/declare.mli | 2 +-
library/declaremods.ml | 2 +-
library/declaremods.mli | 2 +-
library/decls.ml | 2 +-
library/decls.mli | 2 +-
library/dischargedhypsmap.ml | 2 +-
library/dischargedhypsmap.mli | 2 +-
library/global.ml | 2 +-
library/global.mli | 2 +-
library/goptions.ml | 2 +-
library/goptions.mli | 2 +-
library/goptionstyp.mli | 2 +-
library/heads.ml | 2 +-
library/heads.mli | 2 +-
library/impargs.ml | 2 +-
library/impargs.mli | 2 +-
library/lib.ml | 2 +-
library/lib.mli | 2 +-
library/libnames.ml | 2 +-
library/libnames.mli | 2 +-
library/libobject.ml | 2 +-
library/libobject.mli | 2 +-
library/library.ml | 2 +-
library/library.mli | 2 +-
library/nameops.ml | 2 +-
library/nameops.mli | 2 +-
library/nametab.ml | 2 +-
library/nametab.mli | 2 +-
library/states.ml | 2 +-
library/states.mli | 2 +-
library/summary.ml | 2 +-
library/summary.mli | 2 +-
parsing/argextend.ml4 | 2 +-
parsing/egrammar.ml | 2 +-
parsing/egrammar.mli | 2 +-
parsing/extend.ml | 2 +-
parsing/extend.mli | 2 +-
parsing/extrawit.ml | 2 +-
parsing/extrawit.mli | 2 +-
parsing/g_constr.ml4 | 2 +-
parsing/g_ltac.ml4 | 3 +-
parsing/g_prim.ml4 | 2 +-
parsing/g_proofs.ml4 | 2 +-
parsing/g_tactic.ml4 | 58 +-
parsing/g_vernac.ml4 | 19 +-
parsing/g_xml.ml4 | 2 +-
parsing/lexer.ml4 | 2 +-
parsing/lexer.mli | 2 +-
parsing/pcoq.ml4 | 2 +-
parsing/pcoq.mli | 2 +-
parsing/ppconstr.ml | 30 +-
parsing/ppconstr.mli | 9 +-
parsing/pptactic.ml | 31 +-
parsing/pptactic.mli | 2 +-
parsing/ppvernac.ml | 22 +-
parsing/ppvernac.mli | 4 +-
parsing/prettyp.ml | 14 +-
parsing/prettyp.mli | 2 +-
parsing/printer.ml | 119 +-
parsing/printer.mli | 6 +-
parsing/printmod.ml | 6 +-
parsing/printmod.mli | 2 +-
parsing/q_constr.ml4 | 2 +-
parsing/q_coqast.ml4 | 24 +-
parsing/q_util.ml4 | 2 +-
parsing/q_util.mli | 2 +-
parsing/tacextend.ml4 | 8 +-
parsing/tactic_printer.ml | 2 +-
parsing/tactic_printer.mli | 2 +-
parsing/tok.ml | 2 +-
parsing/tok.mli | 2 +-
parsing/vernacextend.ml4 | 13 +-
plugins/cc/ccalgo.ml | 2 +-
plugins/cc/ccalgo.mli | 2 +-
plugins/cc/ccproof.ml | 2 +-
plugins/cc/ccproof.mli | 2 +-
plugins/cc/cctac.ml | 8 +-
plugins/cc/cctac.mli | 2 +-
plugins/cc/g_congruence.ml4 | 2 +-
plugins/decl_mode/decl_expr.mli | 2 +-
plugins/decl_mode/decl_interp.ml | 2 +-
plugins/decl_mode/decl_interp.mli | 2 +-
plugins/decl_mode/decl_mode.ml | 2 +-
plugins/decl_mode/decl_mode.mli | 2 +-
plugins/decl_mode/decl_proof_instr.ml | 2 +-
plugins/decl_mode/decl_proof_instr.mli | 2 +-
plugins/decl_mode/g_decl_mode.ml4 | 2 +-
plugins/decl_mode/ppdecl_proof.ml | 2 +-
plugins/extraction/ExtrOcamlBasic.v | 2 +-
plugins/extraction/ExtrOcamlBigIntConv.v | 2 +-
plugins/extraction/ExtrOcamlIntConv.v | 2 +-
plugins/extraction/ExtrOcamlNatBigInt.v | 2 +-
plugins/extraction/ExtrOcamlNatInt.v | 2 +-
plugins/extraction/ExtrOcamlString.v | 2 +-
plugins/extraction/ExtrOcamlZBigInt.v | 8 +-
plugins/extraction/ExtrOcamlZInt.v | 4 +-
plugins/extraction/big.ml | 2 +-
plugins/extraction/common.ml | 4 +-
plugins/extraction/common.mli | 2 +-
plugins/extraction/extract_env.ml | 6 +-
plugins/extraction/extract_env.mli | 2 +-
plugins/extraction/extraction.ml | 2 +-
plugins/extraction/extraction.mli | 2 +-
plugins/extraction/g_extraction.ml4 | 2 +-
plugins/extraction/haskell.ml | 2 +-
plugins/extraction/haskell.mli | 2 +-
plugins/extraction/miniml.mli | 2 +-
plugins/extraction/mlutil.ml | 2 +-
plugins/extraction/mlutil.mli | 2 +-
plugins/extraction/modutil.ml | 2 +-
plugins/extraction/modutil.mli | 2 +-
plugins/extraction/ocaml.ml | 2 +-
plugins/extraction/ocaml.mli | 2 +-
plugins/extraction/scheme.ml | 2 +-
plugins/extraction/scheme.mli | 2 +-
plugins/extraction/table.ml | 3 +-
plugins/extraction/table.mli | 2 +-
plugins/field/LegacyField.v | 2 +-
plugins/field/LegacyField_Compl.v | 2 +-
plugins/field/LegacyField_Tactic.v | 22 +-
plugins/field/LegacyField_Theory.v | 182 +-
plugins/field/field.ml4 | 2 +-
plugins/firstorder/formula.ml | 2 +-
plugins/firstorder/formula.mli | 2 +-
plugins/firstorder/g_ground.ml4 | 2 +-
plugins/firstorder/ground.ml | 2 +-
plugins/firstorder/ground.mli | 2 +-
plugins/firstorder/instances.ml | 2 +-
plugins/firstorder/instances.mli | 2 +-
plugins/firstorder/rules.ml | 2 +-
plugins/firstorder/rules.mli | 2 +-
plugins/firstorder/sequent.ml | 2 +-
plugins/firstorder/sequent.mli | 2 +-
plugins/firstorder/unify.ml | 2 +-
plugins/firstorder/unify.mli | 2 +-
plugins/fourier/Fourier.v | 2 +-
plugins/fourier/Fourier_util.v | 34 +-
plugins/fourier/fourier.ml | 2 +-
plugins/fourier/fourierR.ml | 2 +-
plugins/fourier/g_fourier.ml4 | 2 +-
plugins/funind/Recdef.v | 2 +-
plugins/funind/functional_principles_types.ml | 6 -
plugins/funind/g_indfun.ml4 | 2 +-
plugins/funind/invfun.ml | 2 +-
plugins/funind/merge.ml | 2 +-
plugins/funind/recdef.ml | 2 +-
plugins/micromega/CheckerMaker.v | 2 +-
plugins/micromega/Env.v | 153 +-
plugins/micromega/EnvRing.v | 1257 +++++--------
plugins/micromega/MExtraction.v | 4 +-
plugins/micromega/OrderedRing.v | 2 +-
plugins/micromega/Psatz.v | 8 +-
plugins/micromega/QMicromega.v | 10 +-
plugins/micromega/RMicromega.v | 30 +-
plugins/micromega/Refl.v | 2 +-
plugins/micromega/RingMicromega.v | 50 +-
plugins/micromega/Tauto.v | 2 +-
plugins/micromega/VarMap.v | 2 +-
plugins/micromega/ZCoeff.v | 16 +-
plugins/micromega/ZMicromega.v | 216 ++-
plugins/micromega/certificate.ml | 2 +-
plugins/micromega/coq_micromega.ml | 23 +-
plugins/micromega/csdpcert.ml | 2 +-
plugins/micromega/g_micromega.ml4 | 2 +-
plugins/micromega/mutils.ml | 2 +-
plugins/micromega/persistent_cache.ml | 32 +-
plugins/micromega/polynomial.ml | 2 +-
plugins/micromega/sos.mli | 2 +-
plugins/micromega/sos_types.ml | 2 +-
plugins/nsatz/Nsatz.v | 40 +-
plugins/nsatz/ideal.ml | 2 +-
plugins/nsatz/nsatz.ml4 | 2 +-
plugins/nsatz/polynom.ml | 2 +-
plugins/nsatz/polynom.mli | 2 +-
plugins/omega/Omega.v | 8 +-
plugins/omega/OmegaLemmas.v | 266 ++-
plugins/omega/OmegaPlugin.v | 2 +-
plugins/omega/PreOmega.v | 353 ++--
plugins/omega/coq_omega.ml | 59 +-
plugins/omega/g_omega.ml4 | 2 +-
plugins/omega/omega.ml | 2 +-
plugins/quote/Quote.v | 4 +-
plugins/quote/g_quote.ml4 | 2 +-
plugins/quote/quote.ml | 2 +-
plugins/ring/LegacyArithRing.v | 8 +-
plugins/ring/LegacyNArithRing.v | 25 +-
plugins/ring/LegacyRing.v | 6 +-
plugins/ring/LegacyRing_theory.v | 42 +-
plugins/ring/LegacyZArithRing.v | 8 +-
plugins/ring/Ring_abstract.v | 90 +-
plugins/ring/Ring_normalize.v | 142 +-
plugins/ring/Setoid_ring.v | 2 +-
plugins/ring/Setoid_ring_normalize.v | 122 +-
plugins/ring/Setoid_ring_theory.v | 4 +-
plugins/ring/g_ring.ml4 | 2 +-
plugins/ring/ring.ml | 8 +-
plugins/romega/ReflOmegaCore.v | 505 +++--
plugins/rtauto/Bintree.v | 16 +-
plugins/rtauto/Rtauto.v | 2 +-
plugins/rtauto/g_rtauto.ml4 | 2 +-
plugins/rtauto/proof_search.ml | 2 +-
plugins/rtauto/proof_search.mli | 2 +-
plugins/rtauto/refl_tauto.ml | 4 +-
plugins/rtauto/refl_tauto.mli | 2 +-
plugins/setoid_ring/ArithRing.v | 10 +-
plugins/setoid_ring/BinList.v | 77 +-
plugins/setoid_ring/Cring.v | 27 +-
plugins/setoid_ring/Field.v | 2 +-
plugins/setoid_ring/Field_tac.v | 6 +-
plugins/setoid_ring/Field_theory.v | 415 ++---
plugins/setoid_ring/InitialRing.v | 108 +-
plugins/setoid_ring/Integral_domain.v | 5 +-
plugins/setoid_ring/NArithRing.v | 2 +-
plugins/setoid_ring/Ncring.v | 35 +-
plugins/setoid_ring/Ncring_initial.v | 56 +-
plugins/setoid_ring/Ncring_polynom.v | 111 +-
plugins/setoid_ring/Ncring_tac.v | 10 +-
plugins/setoid_ring/RealField.v | 64 +-
plugins/setoid_ring/Ring.v | 4 +-
plugins/setoid_ring/Ring_base.v | 2 +-
plugins/setoid_ring/Ring_polynom.v | 1310 +++++--------
plugins/setoid_ring/Ring_tac.v | 7 +-
plugins/setoid_ring/Ring_theory.v | 293 ++-
plugins/setoid_ring/Rings_Z.v | 2 +-
plugins/setoid_ring/ZArithRing.v | 6 +-
plugins/setoid_ring/newring.ml4 | 2 +-
plugins/subtac/eterm.mli | 2 +-
plugins/subtac/g_subtac.ml4 | 2 +-
plugins/subtac/subtac.ml | 2 +-
plugins/subtac/subtac_cases.ml | 2 +-
plugins/subtac/subtac_cases.mli | 2 +-
plugins/subtac/subtac_classes.ml | 2 +-
plugins/subtac/subtac_classes.mli | 2 +-
plugins/subtac/subtac_coercion.ml | 2 +-
plugins/subtac/subtac_command.ml | 9 +-
plugins/subtac/subtac_pretyping.ml | 2 +-
plugins/subtac/subtac_pretyping_F.ml | 2 +-
plugins/syntax/nat_syntax.ml | 6 +-
plugins/syntax/numbers_syntax.ml | 96 +-
plugins/syntax/r_syntax.ml | 2 +-
plugins/syntax/z_syntax.ml | 2 +-
plugins/xml/dumptree.ml4 | 2 +-
pretyping/arguments_renaming.ml | 2 +-
pretyping/arguments_renaming.mli | 2 +-
pretyping/cases.ml | 2 +-
pretyping/cases.mli | 2 +-
pretyping/cbv.ml | 2 +-
pretyping/cbv.mli | 2 +-
pretyping/classops.ml | 2 +-
pretyping/classops.mli | 2 +-
pretyping/coercion.ml | 2 +-
pretyping/coercion.mli | 2 +-
pretyping/detyping.ml | 2 +-
pretyping/detyping.mli | 2 +-
pretyping/evarconv.ml | 36 +-
pretyping/evarconv.mli | 2 +-
pretyping/evarutil.ml | 85 +-
pretyping/evarutil.mli | 24 +-
pretyping/evd.ml | 2 +-
pretyping/evd.mli | 2 +-
pretyping/glob_term.ml | 2 +-
pretyping/glob_term.mli | 2 +-
pretyping/indrec.ml | 2 +-
pretyping/indrec.mli | 2 +-
pretyping/inductiveops.ml | 2 +-
pretyping/inductiveops.mli | 2 +-
pretyping/matching.ml | 2 +-
pretyping/matching.mli | 2 +-
pretyping/namegen.ml | 2 +-
pretyping/namegen.mli | 2 +-
pretyping/pattern.ml | 2 +-
pretyping/pattern.mli | 2 +-
pretyping/pretype_errors.ml | 2 +-
pretyping/pretype_errors.mli | 2 +-
pretyping/pretyping.ml | 16 +-
pretyping/pretyping.mli | 2 +-
pretyping/recordops.ml | 2 +-
pretyping/recordops.mli | 2 +-
pretyping/reductionops.ml | 2 +-
pretyping/reductionops.mli | 2 +-
pretyping/retyping.ml | 2 +-
pretyping/retyping.mli | 2 +-
pretyping/tacred.ml | 2 +-
pretyping/tacred.mli | 2 +-
pretyping/term_dnet.ml | 2 +-
pretyping/term_dnet.mli | 2 +-
pretyping/termops.ml | 2 +-
pretyping/termops.mli | 2 +-
pretyping/typeclasses.ml | 2 +-
pretyping/typeclasses.mli | 2 +-
pretyping/typeclasses_errors.ml | 2 +-
pretyping/typeclasses_errors.mli | 2 +-
pretyping/typing.ml | 2 +-
pretyping/typing.mli | 2 +-
pretyping/unification.ml | 26 +-
pretyping/unification.mli | 2 +-
pretyping/vnorm.ml | 2 +-
pretyping/vnorm.mli | 2 +-
proofs/clenv.ml | 2 +-
proofs/clenv.mli | 2 +-
proofs/clenvtac.ml | 6 +-
proofs/clenvtac.mli | 2 +-
proofs/evar_refiner.ml | 2 +-
proofs/evar_refiner.mli | 2 +-
proofs/goal.ml | 2 +-
proofs/goal.mli | 2 +-
proofs/logic.ml | 2 +-
proofs/logic.mli | 2 +-
proofs/pfedit.ml | 5 +-
proofs/pfedit.mli | 2 +-
proofs/proof.ml | 18 +-
proofs/proof.mli | 11 +-
proofs/proof_global.ml | 2 +-
proofs/proof_global.mli | 2 +-
proofs/proof_type.ml | 2 +-
proofs/proof_type.mli | 2 +-
proofs/proofview.ml | 7 +-
proofs/proofview.mli | 20 +-
proofs/redexpr.ml | 2 +-
proofs/redexpr.mli | 2 +-
proofs/refiner.ml | 2 +-
proofs/refiner.mli | 2 +-
proofs/tacexpr.ml | 14 +-
proofs/tacmach.ml | 2 +-
proofs/tacmach.mli | 2 +-
proofs/tactic_debug.ml | 2 +-
proofs/tactic_debug.mli | 2 +-
scripts/coqc.ml | 2 +-
scripts/coqmktop.ml | 41 +-
states/MakeInitial.v | 2 +-
tactics/auto.ml | 26 +-
tactics/auto.mli | 2 +-
tactics/autorewrite.ml | 2 +-
tactics/autorewrite.mli | 2 +-
tactics/btermdn.ml | 2 +-
tactics/btermdn.mli | 2 +-
tactics/class_tactics.ml4 | 2 +-
tactics/contradiction.ml | 2 +-
tactics/contradiction.mli | 2 +-
tactics/eauto.ml4 | 2 +-
tactics/eauto.mli | 2 +-
tactics/elim.ml | 2 +-
tactics/elim.mli | 2 +-
tactics/elimschemes.ml | 2 +-
tactics/elimschemes.mli | 2 +-
tactics/eqdecide.ml4 | 2 +-
tactics/eqschemes.ml | 2 +-
tactics/eqschemes.mli | 2 +-
tactics/equality.ml | 2 +-
tactics/equality.mli | 2 +-
tactics/evar_tactics.ml | 2 +-
tactics/evar_tactics.mli | 2 +-
tactics/extraargs.ml4 | 2 +-
tactics/extraargs.mli | 2 +-
tactics/extratactics.ml4 | 8 +-
tactics/extratactics.mli | 2 +-
tactics/hiddentac.ml | 25 +-
tactics/hiddentac.mli | 21 +-
tactics/hipattern.ml4 | 2 +-
tactics/hipattern.mli | 2 +-
tactics/inv.ml | 2 +-
tactics/inv.mli | 2 +-
tactics/leminv.ml | 2 +-
tactics/nbtermdn.ml | 2 +-
tactics/nbtermdn.mli | 2 +-
tactics/refine.ml | 2 +-
tactics/refine.mli | 2 +-
tactics/rewrite.ml4 | 247 ++-
tactics/tacinterp.ml | 65 +-
tactics/tacinterp.mli | 3 +-
tactics/tactic_option.ml | 2 +-
tactics/tactic_option.mli | 2 +-
tactics/tacticals.ml | 2 +-
tactics/tacticals.mli | 2 +-
tactics/tactics.ml | 21 +-
tactics/tactics.mli | 6 +-
tactics/tauto.ml4 | 2 +-
tactics/termdn.ml | 2 +-
tactics/termdn.mli | 2 +-
test-suite/bench/lists-100.v | 2 +-
test-suite/bench/lists_100.v | 2 +-
test-suite/bugs/closed/shouldsucceed/1414.v | 4 +-
test-suite/bugs/closed/shouldsucceed/1784.v | 2 +-
test-suite/bugs/closed/shouldsucceed/1844.v | 2 +-
test-suite/bugs/closed/shouldsucceed/1935.v | 2 +-
test-suite/bugs/closed/shouldsucceed/2127.v | 4 +-
test-suite/bugs/closed/shouldsucceed/2817.v | 9 +
test-suite/bugs/closed/shouldsucceed/2836.v | 39 +
test-suite/complexity/ring2.v | 7 +-
test-suite/failure/Tauto.v | 2 +-
test-suite/failure/Uminus.v | 4 +-
test-suite/failure/clash_cons.v | 2 +-
test-suite/failure/fixpoint1.v | 2 +-
test-suite/failure/guard.v | 2 +-
test-suite/failure/illtype1.v | 2 +-
test-suite/failure/pattern.v | 2 +-
test-suite/failure/positivity.v | 2 +-
test-suite/failure/redef.v | 2 +-
test-suite/failure/search.v | 2 +-
test-suite/failure/subtyping2.v | 20 +-
test-suite/failure/universes-buraliforti-redef.v | 20 +-
test-suite/failure/universes-buraliforti.v | 20 +-
test-suite/ideal-features/Apply.v | 2 +-
test-suite/ideal-features/eapply_evar.v | 2 +-
test-suite/micromega/example.v | 10 +-
test-suite/micromega/square.v | 18 +-
test-suite/misc/berardi_test.v | 14 +-
test-suite/modules/PO.v | 4 +-
test-suite/modules/Przyklad.v | 14 +-
test-suite/output/Notations.out | 5 +
test-suite/output/Notations.v | 9 +
test-suite/output/ZSyntax.out | 14 +-
test-suite/success/Check.v | 2 +-
test-suite/success/Field.v | 2 +-
test-suite/success/Funind.v | 22 +-
test-suite/success/Hints.v | 26 +-
test-suite/success/LegacyField.v | 2 +-
test-suite/success/MatchFail.v | 4 +-
test-suite/success/Mod_type.v | 12 +
test-suite/success/Notations.v | 5 +
test-suite/success/OmegaPre.v | 16 +-
test-suite/success/ProgramWf.v | 6 +-
test-suite/success/ROmegaPre.v | 16 +-
test-suite/success/RecTutorial.v | 10 +-
test-suite/success/Reg.v | 8 +-
test-suite/success/Scopes.v | 2 +-
test-suite/success/Tauto.v | 2 +-
test-suite/success/TestRefine.v | 2 +-
test-suite/success/Try.v | 2 +-
test-suite/success/apply.v | 6 +-
test-suite/success/change.v | 6 +-
test-suite/success/decl_mode.v | 10 +-
test-suite/success/dependentind.v | 2 +-
test-suite/success/eauto.v | 2 +-
test-suite/success/eqdecide.v | 2 +-
test-suite/success/extraction.v | 2 +-
test-suite/success/fix.v | 8 +-
test-suite/success/inds_type_sec.v | 2 +-
test-suite/success/induct.v | 2 +-
test-suite/success/ltac.v | 8 +-
test-suite/success/mutual_ind.v | 2 +-
test-suite/success/proof_using.v | 6 +
test-suite/success/remember.v | 2 +-
test-suite/success/searchabout.v | 2 +-
test-suite/success/setoid_test.v | 20 +-
test-suite/success/specialize.v | 28 +-
test-suite/success/unfold.v | 2 +-
test-suite/success/unicode_utf8.v | 2 +-
test-suite/success/univers.v | 4 +-
test-suite/typeclasses/NewSetoid.v | 2 +-
theories/Arith/Arith.v | 2 +-
theories/Arith/Arith_base.v | 2 +-
theories/Arith/Between.v | 8 +-
theories/Arith/Bool_nat.v | 4 +-
theories/Arith/Compare.v | 8 +-
theories/Arith/Compare_dec.v | 10 +-
theories/Arith/Div2.v | 18 +-
theories/Arith/EqNat.v | 18 +-
theories/Arith/Euclid.v | 20 +-
theories/Arith/Even.v | 6 +-
theories/Arith/Factorial.v | 8 +-
theories/Arith/Gt.v | 16 +-
theories/Arith/Le.v | 8 +-
theories/Arith/Lt.v | 12 +-
theories/Arith/Max.v | 2 +-
theories/Arith/Min.v | 4 +-
theories/Arith/Minus.v | 32 +-
theories/Arith/Mult.v | 24 +-
theories/Arith/Peano_dec.v | 6 +-
theories/Arith/Plus.v | 32 +-
theories/Arith/Wf_nat.v | 22 +-
theories/Bool/Bool.v | 8 +-
theories/Bool/BoolEq.v | 6 +-
theories/Bool/Bvector.v | 4 +-
theories/Bool/DecBool.v | 2 +-
theories/Bool/IfProp.v | 2 +-
theories/Bool/Sumbool.v | 2 +-
theories/Bool/Zerob.v | 4 +-
theories/Classes/EquivDec.v | 4 +-
theories/Classes/Equivalence.v | 6 +-
theories/Classes/Init.v | 2 +-
theories/Classes/Morphisms.v | 4 +-
theories/Classes/Morphisms_Prop.v | 2 +-
theories/Classes/Morphisms_Relations.v | 2 +-
theories/Classes/RelationClasses.v | 4 +-
theories/Classes/SetoidClass.v | 2 +-
theories/Classes/SetoidDec.v | 4 +-
theories/Classes/SetoidTactics.v | 4 +-
theories/FSets/FMapAVL.v | 20 +-
theories/FSets/FMapFullAVL.v | 4 +-
theories/FSets/FMapPositive.v | 2 +-
theories/FSets/FSetBridge.v | 148 +-
theories/FSets/FSetEqProperties.v | 8 +-
theories/FSets/FSetFacts.v | 6 +-
theories/FSets/FSetProperties.v | 2 +-
theories/Init/Datatypes.v | 24 +-
theories/Init/Logic.v | 24 +-
theories/Init/Logic_Type.v | 12 +-
theories/Init/Notations.v | 2 +-
theories/Init/Peano.v | 26 +-
theories/Init/Prelude.v | 2 +-
theories/Init/Specif.v | 28 +-
theories/Init/Tactics.v | 12 +-
theories/Init/Wf.v | 4 +-
theories/Lists/List.v | 48 +-
theories/Lists/ListSet.v | 78 +-
theories/Lists/ListTactics.v | 4 +-
theories/Lists/SetoidList.v | 90 +-
theories/Lists/SetoidPermutation.v | 125 ++
theories/Lists/StreamMemo.v | 29 +-
theories/Lists/Streams.v | 14 +-
theories/Lists/vo.itarget | 1 +
theories/Logic/Berardi.v | 14 +-
theories/Logic/ChoiceFacts.v | 6 +-
theories/Logic/Classical.v | 2 +-
theories/Logic/ClassicalChoice.v | 2 +-
theories/Logic/ClassicalDescription.v | 4 +-
theories/Logic/ClassicalEpsilon.v | 2 +-
theories/Logic/ClassicalFacts.v | 38 +-
theories/Logic/ClassicalUniqueChoice.v | 2 +-
theories/Logic/Classical_Pred_Set.v | 2 +-
theories/Logic/Classical_Pred_Type.v | 10 +-
theories/Logic/Classical_Prop.v | 10 +-
theories/Logic/Classical_Type.v | 2 +-
theories/Logic/ConstructiveEpsilon.v | 6 +-
theories/Logic/Decidable.v | 2 +-
theories/Logic/Description.v | 2 +-
theories/Logic/Diaconescu.v | 16 +-
theories/Logic/Epsilon.v | 2 +-
theories/Logic/Eqdep.v | 2 +-
theories/Logic/EqdepFacts.v | 14 +-
theories/Logic/Eqdep_dec.v | 32 +-
theories/Logic/ExtensionalityFacts.v | 2 +-
theories/Logic/FunctionalExtensionality.v | 2 +-
theories/Logic/Hurkens.v | 6 +-
theories/Logic/IndefiniteDescription.v | 2 +-
theories/Logic/JMeq.v | 2 +-
theories/Logic/ProofIrrelevance.v | 2 +-
theories/Logic/ProofIrrelevanceFacts.v | 4 +-
theories/Logic/RelationalChoice.v | 2 +-
theories/Logic/SetIsType.v | 2 +-
theories/MSets/MSetEqProperties.v | 8 +-
theories/MSets/MSetInterface.v | 2 +-
theories/MSets/MSetList.v | 6 +-
theories/MSets/MSetPositive.v | 4 +-
theories/MSets/MSetProperties.v | 2 +-
theories/MSets/MSetRBT.v | 104 +-
theories/MSets/MSetWeakList.v | 6 +-
theories/NArith/BinNat.v | 220 +--
theories/NArith/BinNatDef.v | 94 +-
theories/NArith/NArith.v | 2 +-
theories/NArith/Ndec.v | 443 ++---
theories/NArith/Ndigits.v | 207 +--
theories/NArith/Ndist.v | 104 +-
theories/NArith/Ndiv_def.v | 14 +-
theories/NArith/Ngcd_def.v | 2 +-
theories/NArith/Nnat.v | 56 +-
theories/NArith/Nsqrt_def.v | 12 +-
theories/Numbers/BigNumPrelude.v | 163 +-
theories/Numbers/BinNums.v | 2 +-
theories/Numbers/Cyclic/Abstract/CyclicAxioms.v | 46 +-
theories/Numbers/Cyclic/Abstract/NZCyclic.v | 14 +-
theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v | 50 +-
theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v | 115 +-
.../Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v | 30 +-
theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v | 272 +--
theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v | 80 +-
theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v | 186 +-
theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v | 88 +-
theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v | 393 ++--
theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v | 26 +-
theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v | 4 +-
theories/Numbers/Cyclic/Int31/Cyclic31.v | 609 +++---
theories/Numbers/Cyclic/Int31/Int31.v | 18 +-
theories/Numbers/Cyclic/Int31/Ring31.v | 4 +-
theories/Numbers/Cyclic/ZModulo/ZModulo.v | 191 +-
theories/Numbers/Integer/Abstract/ZAdd.v | 2 +-
theories/Numbers/Integer/Abstract/ZAddOrder.v | 2 +-
theories/Numbers/Integer/Abstract/ZAxioms.v | 2 +-
theories/Numbers/Integer/Abstract/ZBase.v | 2 +-
theories/Numbers/Integer/Abstract/ZBits.v | 4 +-
theories/Numbers/Integer/Abstract/ZDivEucl.v | 2 +-
theories/Numbers/Integer/Abstract/ZDivFloor.v | 4 +-
theories/Numbers/Integer/Abstract/ZDivTrunc.v | 2 +-
theories/Numbers/Integer/Abstract/ZGcd.v | 2 +-
theories/Numbers/Integer/Abstract/ZLcm.v | 2 +-
theories/Numbers/Integer/Abstract/ZLt.v | 2 +-
theories/Numbers/Integer/Abstract/ZMaxMin.v | 2 +-
theories/Numbers/Integer/Abstract/ZMul.v | 2 +-
theories/Numbers/Integer/Abstract/ZMulOrder.v | 2 +-
theories/Numbers/Integer/Abstract/ZParity.v | 2 +-
theories/Numbers/Integer/Abstract/ZPow.v | 13 +-
theories/Numbers/Integer/Abstract/ZProperties.v | 2 +-
theories/Numbers/Integer/Abstract/ZSgnAbs.v | 2 +-
theories/Numbers/Integer/BigZ/BigZ.v | 10 +-
theories/Numbers/Integer/BigZ/ZMake.v | 454 ++---
theories/Numbers/Integer/Binary/ZBinary.v | 4 +-
theories/Numbers/Integer/NatPairs/ZNatPairs.v | 4 +-
theories/Numbers/Integer/SpecViaZ/ZSig.v | 2 +-
theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v | 6 +-
theories/Numbers/NaryFunctions.v | 2 +-
theories/Numbers/NatInt/NZAdd.v | 2 +-
theories/Numbers/NatInt/NZAddOrder.v | 2 +-
theories/Numbers/NatInt/NZAxioms.v | 4 +-
theories/Numbers/NatInt/NZBase.v | 2 +-
theories/Numbers/NatInt/NZBits.v | 2 +-
theories/Numbers/NatInt/NZDiv.v | 2 +-
theories/Numbers/NatInt/NZDomain.v | 2 +-
theories/Numbers/NatInt/NZGcd.v | 2 +-
theories/Numbers/NatInt/NZLog.v | 2 +-
theories/Numbers/NatInt/NZMul.v | 2 +-
theories/Numbers/NatInt/NZMulOrder.v | 6 +-
theories/Numbers/NatInt/NZOrder.v | 2 +-
theories/Numbers/NatInt/NZParity.v | 2 +-
theories/Numbers/NatInt/NZPow.v | 2 +-
theories/Numbers/NatInt/NZProperties.v | 2 +-
theories/Numbers/NatInt/NZSqrt.v | 2 +-
theories/Numbers/Natural/Abstract/NAdd.v | 2 +-
theories/Numbers/Natural/Abstract/NAddOrder.v | 2 +-
theories/Numbers/Natural/Abstract/NAxioms.v | 2 +-
theories/Numbers/Natural/Abstract/NBase.v | 2 +-
theories/Numbers/Natural/Abstract/NBits.v | 4 +-
theories/Numbers/Natural/Abstract/NDefOps.v | 4 +-
theories/Numbers/Natural/Abstract/NDiv.v | 2 +-
theories/Numbers/Natural/Abstract/NGcd.v | 2 +-
theories/Numbers/Natural/Abstract/NIso.v | 2 +-
theories/Numbers/Natural/Abstract/NLcm.v | 2 +-
theories/Numbers/Natural/Abstract/NLog.v | 2 +-
theories/Numbers/Natural/Abstract/NMaxMin.v | 2 +-
theories/Numbers/Natural/Abstract/NMulOrder.v | 2 +-
theories/Numbers/Natural/Abstract/NOrder.v | 2 +-
theories/Numbers/Natural/Abstract/NParity.v | 2 +-
theories/Numbers/Natural/Abstract/NPow.v | 2 +-
theories/Numbers/Natural/Abstract/NProperties.v | 2 +-
theories/Numbers/Natural/Abstract/NSqrt.v | 2 +-
theories/Numbers/Natural/Abstract/NStrongRec.v | 2 +-
theories/Numbers/Natural/Abstract/NSub.v | 2 +-
theories/Numbers/Natural/BigN/BigN.v | 4 +-
theories/Numbers/Natural/BigN/NMake.v | 364 ++--
theories/Numbers/Natural/BigN/NMake_gen.ml | 2 +-
theories/Numbers/Natural/BigN/Nbasic.v | 120 +-
theories/Numbers/Natural/Binary/NBinary.v | 6 +-
theories/Numbers/Natural/Peano/NPeano.v | 2 +-
theories/Numbers/Natural/SpecViaZ/NSig.v | 2 +-
theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 10 +-
theories/Numbers/NumPrelude.v | 2 +-
theories/Numbers/Rational/BigQ/BigQ.v | 10 +-
theories/Numbers/Rational/BigQ/QMake.v | 485 +++--
theories/Numbers/Rational/SpecViaQ/QSig.v | 2 +-
theories/PArith/BinPos.v | 364 ++--
theories/PArith/BinPosDef.v | 5 +-
theories/PArith/PArith.v | 2 +-
theories/PArith/POrderedType.v | 2 +-
theories/PArith/Pnat.v | 81 +-
theories/Program/Basics.v | 4 +-
theories/Program/Combinators.v | 2 +-
theories/Program/Equality.v | 12 +-
theories/Program/Program.v | 2 +-
theories/Program/Subset.v | 6 +-
theories/Program/Syntax.v | 2 +-
theories/Program/Tactics.v | 4 +-
theories/Program/Utils.v | 2 +-
theories/Program/Wf.v | 6 +-
theories/QArith/QArith.v | 2 +-
theories/QArith/QArith_base.v | 255 ++-
theories/QArith/QOrderedType.v | 2 +-
theories/QArith/Qabs.v | 26 +-
theories/QArith/Qcanon.v | 22 +-
theories/QArith/Qfield.v | 6 +-
theories/QArith/Qminmax.v | 2 +-
theories/QArith/Qpower.v | 88 +-
theories/QArith/Qreals.v | 62 +-
theories/QArith/Qreduction.v | 166 +-
theories/QArith/Qring.v | 2 +-
theories/QArith/Qround.v | 26 +-
theories/Reals/Alembert.v | 254 +--
theories/Reals/AltSeries.v | 122 +-
theories/Reals/ArithProp.v | 50 +-
theories/Reals/Binomial.v | 68 +-
theories/Reals/Cauchy_prod.v | 28 +-
theories/Reals/Cos_plus.v | 194 +-
theories/Reals/Cos_rel.v | 92 +-
theories/Reals/DiscrR.v | 10 +-
theories/Reals/Exp_prop.v | 230 ++-
theories/Reals/Integration.v | 2 +-
theories/Reals/LegacyRfield.v | 6 +-
theories/Reals/MVT.v | 102 +-
theories/Reals/Machin.v | 168 ++
theories/Reals/NewtonInt.v | 158 +-
theories/Reals/PSeries_reg.v | 62 +-
theories/Reals/PartSum.v | 142 +-
theories/Reals/RIneq.v | 266 +--
theories/Reals/RList.v | 232 +--
theories/Reals/ROrderedType.v | 2 +-
theories/Reals/R_Ifp.v | 80 +-
theories/Reals/R_sqr.v | 36 +-
theories/Reals/R_sqrt.v | 56 +-
theories/Reals/Ranalysis.v | 775 +-------
theories/Reals/Ranalysis1.v | 362 ++--
theories/Reals/Ranalysis2.v | 92 +-
theories/Reals/Ranalysis3.v | 162 +-
theories/Reals/Ranalysis4.v | 106 +-
theories/Reals/Ranalysis5.v | 1348 ++++++++++++++
theories/Reals/Ranalysis_reg.v | 800 ++++++++
theories/Reals/Ratan.v | 1602 ++++++++++++++++
theories/Reals/Raxioms.v | 8 +-
theories/Reals/Rbase.v | 2 +-
theories/Reals/Rbasic_fun.v | 102 +-
theories/Reals/Rcomplete.v | 50 +-
theories/Reals/Rdefinitions.v | 4 +-
theories/Reals/Rderiv.v | 114 +-
theories/Reals/Reals.v | 2 +-
theories/Reals/Rfunctions.v | 119 +-
theories/Reals/Rgeom.v | 32 +-
theories/Reals/RiemannInt.v | 898 ++++-----
theories/Reals/RiemannInt_SF.v | 954 +++++-----
theories/Reals/Rlimit.v | 106 +-
theories/Reals/Rlogic.v | 10 +-
theories/Reals/Rminmax.v | 2 +-
theories/Reals/Rpow_def.v | 2 +-
theories/Reals/Rpower.v | 168 +-
theories/Reals/Rprod.v | 20 +-
theories/Reals/Rseries.v | 44 +-
theories/Reals/Rsigma.v | 34 +-
theories/Reals/Rsqrt_def.v | 216 +--
theories/Reals/Rtopology.v | 694 +++----
theories/Reals/Rtrigo.v | 1796 +-----------------
theories/Reals/Rtrigo1.v | 1933 ++++++++++++++++++++
theories/Reals/Rtrigo_alt.v | 163 +-
theories/Reals/Rtrigo_calc.v | 112 +-
theories/Reals/Rtrigo_def.v | 108 +-
theories/Reals/Rtrigo_fun.v | 30 +-
theories/Reals/Rtrigo_reg.v | 308 +---
theories/Reals/SeqProp.v | 270 +--
theories/Reals/SeqSeries.v | 98 +-
theories/Reals/SplitAbsolu.v | 4 +-
theories/Reals/SplitRmult.v | 2 +-
theories/Reals/Sqrt_reg.v | 150 +-
theories/Reals/vo.itarget | 5 +
theories/Relations/Operators_Properties.v | 8 +-
theories/Relations/Relation_Definitions.v | 2 +-
theories/Relations/Relation_Operators.v | 8 +-
theories/Relations/Relations.v | 8 +-
theories/Setoids/Setoid.v | 2 +-
theories/Sets/Classical_sets.v | 18 +-
theories/Sets/Constructive_sets.v | 18 +-
theories/Sets/Cpo.v | 2 +-
theories/Sets/Ensembles.v | 2 +-
theories/Sets/Finite_sets.v | 6 +-
theories/Sets/Finite_sets_facts.v | 20 +-
theories/Sets/Image.v | 12 +-
theories/Sets/Infinite_sets.v | 14 +-
theories/Sets/Integers.v | 24 +-
theories/Sets/Multiset.v | 18 +-
theories/Sets/Partial_Order.v | 20 +-
theories/Sets/Permut.v | 2 +-
theories/Sets/Powerset.v | 28 +-
theories/Sets/Powerset_Classical_facts.v | 42 +-
theories/Sets/Powerset_facts.v | 36 +-
theories/Sets/Relations_1.v | 2 +-
theories/Sets/Relations_1_facts.v | 20 +-
theories/Sets/Relations_2.v | 2 +-
theories/Sets/Relations_2_facts.v | 14 +-
theories/Sets/Relations_3.v | 2 +-
theories/Sets/Relations_3_facts.v | 28 +-
theories/Sets/Uniset.v | 30 +-
theories/Sorting/Heap.v | 22 +-
theories/Sorting/Mergesort.v | 4 +-
theories/Sorting/PermutEq.v | 2 +-
theories/Sorting/PermutSetoid.v | 12 +-
theories/Sorting/Permutation.v | 2 +-
theories/Sorting/Sorted.v | 2 +-
theories/Sorting/Sorting.v | 2 +-
theories/Strings/Ascii.v | 16 +-
theories/Strings/String.v | 130 +-
theories/Structures/DecidableTypeEx.v | 6 +-
theories/Structures/OrderedTypeEx.v | 160 +-
theories/Structures/OrdersAlt.v | 6 +-
theories/Unicode/Utf8.v | 4 +-
theories/Unicode/Utf8_core.v | 2 +-
theories/Vectors/VectorDef.v | 2 +-
theories/Wellfounded/Disjoint_Union.v | 4 +-
theories/Wellfounded/Inclusion.v | 4 +-
theories/Wellfounded/Inverse_Image.v | 6 +-
.../Wellfounded/Lexicographic_Exponentiation.v | 28 +-
theories/Wellfounded/Lexicographic_Product.v | 10 +-
theories/Wellfounded/Transitive_Closure.v | 6 +-
theories/Wellfounded/Union.v | 6 +-
theories/Wellfounded/Well_Ordering.v | 8 +-
theories/Wellfounded/Wellfounded.v | 2 +-
theories/ZArith/BinInt.v | 804 ++++----
theories/ZArith/BinIntDef.v | 253 +--
theories/ZArith/Int.v | 16 +-
theories/ZArith/Wf_Z.v | 12 +-
theories/ZArith/ZArith.v | 2 +-
theories/ZArith/ZArith_base.v | 2 +-
theories/ZArith/ZArith_dec.v | 93 +-
theories/ZArith/Zabs.v | 56 +-
theories/ZArith/Zbool.v | 16 +-
theories/ZArith/Zcompare.v | 34 +-
theories/ZArith/Zcomplements.v | 14 +-
theories/ZArith/Zdigits.v | 58 +-
theories/ZArith/Zdiv.v | 86 +-
theories/ZArith/Zeuclid.v | 2 +-
theories/ZArith/Zeven.v | 22 +-
theories/ZArith/Zgcd_alt.v | 241 ++-
theories/ZArith/Zhints.v | 95 +-
theories/ZArith/Zlogarithm.v | 104 +-
theories/ZArith/Zmax.v | 121 +-
theories/ZArith/Zmin.v | 92 +-
theories/ZArith/Zminmax.v | 16 +-
theories/ZArith/Zmisc.v | 11 +-
theories/ZArith/Znat.v | 162 +-
theories/ZArith/Znumtheory.v | 385 ++--
theories/ZArith/Zorder.v | 100 +-
theories/ZArith/Zpow_alt.v | 4 +-
theories/ZArith/Zpow_def.v | 14 +-
theories/ZArith/Zpow_facts.v | 42 +-
theories/ZArith/Zpower.v | 14 +-
theories/ZArith/Zquot.v | 351 ++--
theories/ZArith/Zsqrt_compat.v | 63 +-
theories/ZArith/Zwf.v | 27 +-
theories/ZArith/auxiliary.v | 2 +-
tools/compat5.ml | 2 +-
tools/compat5.mlp | 2 +-
tools/compat5b.ml | 2 +-
tools/compat5b.mlp | 2 +-
tools/coq_makefile.ml | 6 +-
tools/coq_tex.ml4 | 2 +-
tools/coqdep.ml | 2 +-
tools/coqdep_boot.ml | 2 +-
tools/coqdep_common.ml | 2 +-
tools/coqdep_common.mli | 2 +-
tools/coqdep_lexer.mli | 2 +-
tools/coqdep_lexer.mll | 2 +-
tools/coqdoc/alpha.ml | 2 +-
tools/coqdoc/alpha.mli | 2 +-
tools/coqdoc/cdglobals.ml | 2 +-
tools/coqdoc/cpretty.mli | 2 +-
tools/coqdoc/cpretty.mll | 71 +-
tools/coqdoc/index.ml | 13 +-
tools/coqdoc/index.mli | 2 +-
tools/coqdoc/main.ml | 2 +-
tools/coqdoc/output.ml | 151 +-
tools/coqdoc/output.mli | 13 +-
tools/coqdoc/tokens.ml | 2 +-
tools/coqdoc/tokens.mli | 2 +-
tools/coqwc.mll | 2 +-
tools/escape_string.ml | 1 +
tools/fake_ide.ml | 2 +-
tools/gallina.ml | 2 +-
tools/gallina_lexer.mll | 2 +-
tools/mingwpath.ml | 15 +
toplevel/auto_ind_decl.ml | 2 +-
toplevel/auto_ind_decl.mli | 2 +-
toplevel/autoinstance.ml | 2 +-
toplevel/autoinstance.mli | 2 +-
toplevel/backtrack.ml | 22 +-
toplevel/backtrack.mli | 10 +-
toplevel/cerrors.ml | 2 +-
toplevel/cerrors.mli | 2 +-
toplevel/class.ml | 2 +-
toplevel/class.mli | 2 +-
toplevel/classes.ml | 2 +-
toplevel/classes.mli | 2 +-
toplevel/command.ml | 9 +-
toplevel/command.mli | 2 +-
toplevel/coqinit.ml | 10 +-
toplevel/coqinit.mli | 4 +-
toplevel/coqtop.ml | 21 +-
toplevel/coqtop.mli | 2 +-
toplevel/discharge.ml | 2 +-
toplevel/discharge.mli | 2 +-
toplevel/himsg.ml | 57 +-
toplevel/himsg.mli | 2 +-
toplevel/ide_intf.ml | 43 +-
toplevel/ide_intf.mli | 2 +-
toplevel/ide_slave.ml | 45 +-
toplevel/ide_slave.mli | 2 +-
toplevel/ind_tables.ml | 2 +-
toplevel/ind_tables.mli | 2 +-
toplevel/indschemes.ml | 2 +-
toplevel/indschemes.mli | 2 +-
toplevel/interface.mli | 16 +-
toplevel/lemmas.ml | 2 +-
toplevel/lemmas.mli | 2 +-
toplevel/libtypes.ml | 2 +-
toplevel/libtypes.mli | 2 +-
toplevel/metasyntax.ml | 20 +-
toplevel/metasyntax.mli | 4 +-
toplevel/mltop.ml4 | 135 +-
toplevel/mltop.mli | 25 +-
toplevel/record.ml | 2 +-
toplevel/record.mli | 2 +-
toplevel/search.ml | 2 +-
toplevel/search.mli | 2 +-
toplevel/toplevel.ml | 2 +-
toplevel/toplevel.mli | 2 +-
toplevel/usage.ml | 4 +-
toplevel/usage.mli | 2 +-
toplevel/vernac.ml | 39 +-
toplevel/vernac.mli | 2 +-
toplevel/vernacentries.ml | 141 +-
toplevel/vernacentries.mli | 4 +-
toplevel/vernacexpr.ml | 18 +-
toplevel/vernacinterp.ml | 2 +-
toplevel/vernacinterp.mli | 2 +-
toplevel/whelp.ml4 | 2 +-
toplevel/whelp.mli | 2 +-
1107 files changed, 21802 insertions(+), 18994 deletions(-)
delete mode 100644 INSTALL.macosx
create mode 100644 TODO
delete mode 100644 config/Makefile.template
create mode 100755 dev/macosify_accel.sh
delete mode 100644 doc/refman/RefMan-sch.tex
create mode 100644 test-suite/bugs/closed/shouldsucceed/2817.v
create mode 100644 test-suite/bugs/closed/shouldsucceed/2836.v
create mode 100644 theories/Lists/SetoidPermutation.v
create mode 100644 theories/Reals/Machin.v
create mode 100644 theories/Reals/Ranalysis5.v
create mode 100644 theories/Reals/Ranalysis_reg.v
create mode 100644 theories/Reals/Ratan.v
create mode 100644 theories/Reals/Rtrigo1.v
create mode 100644 tools/escape_string.ml
create mode 100644 tools/mingwpath.ml
(limited to 'plugins/setoid_ring')
diff --git a/.gitignore b/.gitignore
index 32a40af6..e0be678c 100644
--- a/.gitignore
+++ b/.gitignore
@@ -63,11 +63,12 @@ doc/refman/csdp.cache
doc/refman/trace
doc/refman/Reference-Manual.pdf
doc/refman/Reference-Manual.ps
+doc/refman/Reference-Manual.html
+doc/refman/Reference-Manual.out
+doc/refman/Reference-Manual.sh
doc/refman/cover.html
doc/refman/styles.hva
-doc/refman/Reference-Manual.html
doc/common/version.tex
-doc/refman/Reference-Manual.sh
doc/refman/coqide-queries.eps
doc/refman/coqide.eps
doc/refman/euclid.ml
diff --git a/CHANGES b/CHANGES
index c245fb25..1c094584 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,29 +1,66 @@
-Changes from V8.4beta to V8.4
-=============================
+Changes from V8.4beta2 to V8.4
+==============================
+
+Vernacular commands
+
+- The "Reset" command is now supported again in files given to coqc or Load.
+- "Show Script" now indents again the displayed scripts. It can also work
+ correctly across Load'ed files if the option "Unset Atomic Load" is used.
+- "Open Scope" can now be given the delimiter (e.g. Z) instead of the full
+ scope name (e.g. Z_scope).
+
+Notations
+
+- Most compatibility notations of the standard library are now tagged as
+ (compat xyz), where xyz is a former Coq version, for instance "8.3".
+ These notations behave as (only parsing) notations, except that they may
+ triggers warnings (or errors) when used while Coq is not in a corresponding
+ -compat mode.
+- To activate these compatibility warnings, use "Set Verbose Compat Notations"
+ or the command-line flag -verbose-compat-notations.
+- For a strict mode without these compatibility notations, use
+ "Unset Compat Notations" or the command-line flag -no-compat-notations.
+
+Tactics
+
+- An annotation "eqn:H" or "eqn:?" can be added to a "destruct"
+ or "induction" to make it generate equations in the spirit of "case_eq".
+ The former syntax "_eqn" is discontinued.
+- The name of the hypothesis introduced by tactic "remember" can be
+ set via the new syntax "remember t as x eqn:H" (wish #2489).
+
+Libraries
+
+- Reals: changed definition of PI, no more axiom about sin(PI/2).
+- SetoidPermutation: a notion of permutation for lists modulo a setoid equality.
+- BigN: fixed the ocaml code doing the parsing/printing of big numbers.
+
+Changes from V8.4beta to V8.4beta2
+==================================
Vernacular commands
-- Undo and UndoTo are now handling the proof states. They may
- perform some extra steps of backtrack to avoid states where
- the proof state is unavailable (typically a closed proof).
-- The commands Suspend and Resume have been removed.
+- Commands "Back" and "BackTo" are now handling the proof states. They may
+ perform some extra steps of backtrack to avoid states where the proof
+ state is unavailable (typically a closed proof).
+- The commands "Suspend" and "Resume" have been removed.
- A basic Show Script has been reintroduced (no indentation).
- New command "Set Parsing Explicit" for deactivating parsing (and printing)
of implicit arguments (useful for teaching).
-- New command "Grab Existential Variables" to transform the unresolved evars at
- the end of a proof into goals.
+- New command "Grab Existential Variables" to transform the unresolved evars
+ at the end of a proof into goals.
Tactics
-- Still no general "info" tactical, but new specific tactics
- info_auto, info_eauto, info_trivial which provides information
- on the proofs found by auto/eauto/trivial. Display of these
- details could also be activated by Set Info Auto/Eauto/Trivial.
-- Details on everything tried by auto/eauto/trivial during
- a proof search could be obtained by "debug auto", "debug eauto",
- "debug trivial" or by a global "Set Debug Auto/Eauto/Trivial".
-- New command "r string" that interprets "idtac string" as a breakpoint
- and jumps to its next use in Ltac debugger.
+- Still no general "info" tactical, but new specific tactics info_auto,
+ info_eauto, info_trivial which provides information on the proofs found
+ by auto/eauto/trivial. Display of these details could also be activated by
+ "Set Info Auto"/"Set Info Eauto"/"Set Info Trivial".
+- Details on everything tried by auto/eauto/trivial during a proof search
+ could be obtained by "debug auto", "debug eauto", "debug trivial" or by a
+ global "Set Debug Auto"/"Set Debug Eauto"/"Set Debug Trivial".
+- New command "r string" in Ltac debugger that interprets "idtac
+ string" in Ltac code as a breakpoint and jumps to its next use.
- Tactics from the Dp plugin (simplify, ergo, yices, cvc3, z3, cvcl,
harvey, zenon, gwhy) have been removed, since Why2 has not been
maintained for the last few years. The Why3 plugin should be a suitable
@@ -31,28 +68,28 @@ Tactics
Libraries
-- MSetRBT : a new implementation of MSets via Red-Black trees (initial
+- MSetRBT: a new implementation of MSets via Red-Black trees (initial
contribution by Andrew Appel).
-- MSetAVL : for maximal sharing with the new MSetRBT, the argument order
- of Node has changed (this should be transparent to regular MSets users).
+- MSetAVL: for maximal sharing with the new MSetRBT, the argument order
+ of Node has changed (this should be transparent to regular MSets users).
Module System
- The names of modules (and module types) are now in a fully separated
- namespace from ordinary definitions : "Definition E:=0. Module E. End E."
+ namespace from ordinary definitions: "Definition E:=0. Module E. End E."
is now accepted.
CoqIDE
-- Coqide now supports the Restart command, and Undo (with a warning).
- Better support for Abort.
+- Coqide now supports the "Restart" command, and "Undo" (with a warning).
+ Better support for "Abort".
Changes from V8.3 to V8.4beta
=============================
Logic
-- Standard eta-conversion now supported (dependent product only). (DOC TO DO)
+- Standard eta-conversion now supported (dependent product only).
- Guard condition improvement: subterm property is propagated through beta-redex
blocked by pattern-matching, as in "(match v with C .. => fun x => u end) x";
this allows for instance to use "rewrite ... in ..." without breaking
@@ -69,10 +106,6 @@ Specification language and notations
- Structure/Record printing can be disable by "Unset Printing Records".
In addition, it can be controlled on type by type basis using
"Add Printing Record" or "Add Printing Constructor".
-- In a pattern containing a "match", a final "| _ => _" branch could be used
- now instead of enumerating all remaining constructors. Moreover, the pattern
- "match _ with _ => _ end" now allows to match any "match". A "in" annotation
- can also be added to restrict to a precise inductive type.
- Pattern-matching compilation algorithm: in "match x, y with ... end",
possible dependencies of x (or of the indices of its type) in the type
of y are now taken into account.
@@ -81,11 +114,11 @@ Tactics
- New proof engine.
- Scripts can now be structured thanks to bullets - * + and to subgoal
- delimitation via { }. Note: for use with ProofGeneral, a cvs version of
- ProofGeneral no older than mid-July 2011 is currently required. DOC TODO.
+ delimitation via { }. Note: for use with Proof General, a cvs version of
+ Proof General no older than mid-July 2011 is currently required.
- Support for tactical "info" is suspended.
- Support for command "Show Script" is suspended.
-- New tactics constr_eq, is_evar and has_evar.
+- New tactics constr_eq, is_evar and has_evar for use in Ltac.
- Removed the two-argument variant of "decide equality".
- New experimental tactical "timeout ". Since is a time
in second for the moment, this feature should rather be avoided
@@ -98,14 +131,14 @@ Tactics
?f x y = g(x,y) (compatibility ensured by using
"Unset Tactic Pattern Unification"). It also supports (full) betaiota.
- Tactic autorewrite does no longer instantiate pre-existing
- existential variables (theoretical source of possible incompatibility).
+ existential variables (theoretical source of possible incompatibilities).
- Tactic "dependent rewrite" now supports equality in "sig".
- Tactic omega now understands Zpred (wish #1912) and can prove any goal
from a context containing an arithmetical contradiction (wish #2236).
- Using "auto with nocore" disables the use of the "core" database (wish #2188).
This pseudo-database "nocore" can also be used with trivial and eauto.
- Tactics "set", "destruct" and "induction" accepts incomplete terms and
- use the goal to complete the pattern assuming it is no ambiguous.
+ use the goal to complete the pattern assuming it is non ambiguous.
- When used on arguments with a dependent type, tactics such as
"destruct", "induction", "case", "elim", etc. now try to abstract
automatically the dependencies over the arguments of the types
@@ -118,18 +151,25 @@ Tactics
- When applying destruct or inversion on a fixpoint hiding an inductive
type, recursive calls to the fixpoint now remain folded by default (rare
source of incompatibility generally solvable by adding a call to simpl).
-- The behavior of the simpl tactic can be tuned using the new "Arguments"
- vernacular.
+- In an ltac pattern containing a "match", a final "| _ => _" branch could be
+ used now instead of enumerating all remaining constructors. Moreover, the
+ pattern "match _ with _ => _ end" now allows to match any "match". A "in"
+ annotation can also be added to restrict to a precise inductive type.
+- The behavior of "simpl" can be tuned using the "Arguments" vernacular.
+ In particular constants can be marked so that they are always/never unfolded
+ by "simpl", or unfolded only when a set of arguments evaluates to a
+ constructor. Last one can mark a constant so that it is unfolded only if the
+ simplified term does not expose a match in head position.
Vernacular commands
- It is now mandatory to have a space (or tabulation or newline or end-of-file)
after a "." ending a sentence.
- In SearchAbout, the [ ] delimiters are now optional.
-- New command "Add/Remove Search Blacklist ..." :
+- New command "Add/Remove Search Blacklist ...":
a Search or SearchAbout or similar query will never mention lemmas
whose qualified names contain any of the declared substrings.
- The default blacklisted substrings are "_admitted" "_subproof" "Private_". DOC TODO
+ The default blacklisted substrings are "_admitted" "_subproof" "Private_".
- When the output file of "Print Universes" ends in ".dot" or ".gv",
the universe graph is printed in the DOT language, and can be
processed by Graphviz tools.
@@ -141,7 +181,11 @@ Vernacular commands
to avoid conversion at Qed time to go into a very long computation.
- New command "Show Goal ident" to display the statement of a goal, even
a closed one (available from Proof General).
-- New command "Arguments" subsuming "Implicit Arguments" and "Arguments Scope".
+- Command "Proof" accept a new modifier "using" to force generalization
+ over a given list of section variables at section ending.
+- New command "Arguments" generalizing "Implicit Arguments" and
+ "Arguments Scope" and that also allows to rename the parameters of a
+ definition and to tune the behavior of the tactic "simpl".
Module System
@@ -155,8 +199,8 @@ Module System
are lower or equal than XX will be inlined.
The level of a parameter can be fixed by "Parameter Inline(30) foo".
When levels aren't given, the default value is 100. One can also use
- the flag "Set Inline Level ..." to set a level. TODO: DOC!
-- Print Assumptions should now handle correctly opaque modules (#2168)
+ the flag "Set Inline Level ..." to set a level.
+- Print Assumptions should now handle correctly opaque modules (#2168).
- Print Module (Type) now tries to print more details, such as types and
bodies of the module elements. Note that Print Module Type could be
used on a module to display only its interface. The option
@@ -166,9 +210,9 @@ Module System
Libraries
- Extension of the abstract part of Numbers, which now provide axiomatizations
- and results about many more integer functions, such as pow, gcd, lcm, sqrt, log2
- and bitwise functions. These functions are implemented for nat N BigN Z BigZ.
- See in particular file NPeano for new functions about nat.
+ and results about many more integer functions, such as pow, gcd, lcm, sqrt,
+ log2 and bitwise functions. These functions are implemented for nat, N, BigN,
+ Z, BigZ. See in particular file NPeano for new functions about nat.
- The definition of types positive, N, Z is now in file BinNums.v
- Major reorganization of ZArith. The initial file ZArith/BinInt.v now contains
an internal module Z implementing the Numbers interface for integers.
@@ -207,15 +251,15 @@ Libraries
may introduce incompatibilities. In particular, the order of the arguments
for BigN.shiftl and BigN.shiftr is now reversed: the number to shift now
comes first. By default, the power function now takes two BigN.
-- Creation of Vector, an independant library for list indiced by their length.
- Vectors' names overwrite lists' one so you shouldn't "Import" the library.
- All old names change: functions' name become the CaML one and for example
- Vcons become Vector.cons. You can use notations by importing
+- Creation of Vector, an independent library for lists indexed by their length.
+ Vectors' names overwrite lists' one so you should not "Import" the library.
+ All old names changed: function names follow the ocaml ones and, for example,
+ Vcons becomes Vector.cons. You can get [..;..;..]-style notations by importing
Vector.VectorNotations.
- Removal of TheoryList. Requiring List instead should work most of the time.
-- New syntax "rew Heq in H" and "rew <- Heq in H" for eq_rect and
+- New syntax "rew Heq in H" and "rew <- Heq in H" for eq_rect and
eq_rect_r (available by importing module EqNotations).
-- Wf.iter_nat is now Peano.nat_iter (with an implicit type argument)
+- Wf.iter_nat is now Peano.nat_iter (with an implicit type argument).
Internal infrastructure
@@ -230,8 +274,8 @@ Internal infrastructure
for both make and ocamlbuild, etc.
- Support of cross-compilation via mingw from unix toward Windows,
contact P. Letouzey for more informations.
-- new Makefile rules mli-doc to make html of mli in dev/doc/html and
- full-stdlib to get a HUGE pdf with all the stdlib.
+- New Makefile rules mli-doc to make html of mli in dev/doc/html and
+ full-stdlib to get a (huge) pdf reflecting the whole standard library.
Extraction
@@ -243,9 +287,8 @@ Extraction
- A new command "Separate Extraction cst1 cst2 ..." that mixes a
minimal extracted environment a la "Recursive Extraction" and the
production of several files (one per coq source) a la "Extraction Library".
- DOC TODO.
- New option "Set/Unset Extraction KeepSingleton" for preventing the
- extraction to optimize singleton container types. DOC TODO
+ extraction to optimize singleton container types.
- The extraction now identifies and properly rejects a particular case of
universe polymorphism it cannot handle yet (the pair (I,I) being Prop).
- Support of anonymous fields in record (#2555).
@@ -257,10 +300,9 @@ CoqIDE
(cf button "Restart Coq", ex-"Go to Start"). For allowing such
interrupts, the Windows version of coqide now requires Windows >= XP
SP1.
-- The communication between CoqIDE and Coqtop is now done via a dialect
- of XML (DOC TODO).
-- The backtrack engine of CoqIDE has been reworked, it now used the
- "Backtrack" command similarly to ProofGeneral.
+- The communication between CoqIDE and Coqtop is now done via a dialect of XML.
+- The backtrack engine of CoqIDE has been reworked, it now uses the
+ "Backtrack" command similarly to Proof General.
- The Coqide parsing of sentences has be reworked and now supports
tactic delimitation via { }.
- Coqide now accepts the Abort command (wish #2357).
@@ -274,15 +316,15 @@ Tools
- Coq now searches directories specified in COQPATH, $XDG_DATA_HOME/coq,
$XDG_DATA_DIRS/coq, and user-contribs before the standard library.
- Coq rc file has moved to $XDG_CONFIG_HOME/coq.
-- coq_makefile major cleanup.
- * mli/mlpack/mllib taken into account, ml not preproccessed anymore, ml4 work
+- Major changes to coq_makefile:
+ * mli/mlpack/mllib taken into account, ml not preproccessed anymore, ml4 work;
* mlihtml generates doc of mli, install-doc install the html doc in DOCDIR
- with the same policy as vo in COQLIB
+ with the same policy as vo in COQLIB;
* More variables are given by coqtop -config, others are defined only if the
users doesn't have defined them elsewhere. Consequently, generated makefile
- should work directly on any architecture.
+ should work directly on any architecture;
* Packagers can take advantage of $(DSTROOT) introduction. Installation can
- be made in $XDG_DATA_HOME/coq.
+ be made in $XDG_DATA_HOME/coq;
* -arg option allows to send option as argument to coqc.
Changes from V8.2 to V8.3
diff --git a/COMPATIBILITY b/COMPATIBILITY
index 0849b64f..41474202 100644
--- a/COMPATIBILITY
+++ b/COMPATIBILITY
@@ -3,4 +3,49 @@ Potential sources of incompatibilities between Coq V8.3 and V8.4
(see also file CHANGES)
-TO BE DONE
+The main known incompatibilities between 8.3 and 8.4 are consequences
+of the following changes:
+
+- The reorganization of the library of numbers:
+
+ Several definitions have new names or are defined in modules of
+ different names, but a special care has been taken to have this
+ renaming transparent for the user thanks to compatibility notations.
+
+ However some definitions have changed, what might require some
+ adaptations. The most noticeable examples are:
+ - The "?=" notation which now bind to Pos.compare rather than former
+ Pcompare (now Pos.compare_cont).
+ - Changes in names may induce different automatically generated
+ names in proof scripts (e.g. when issuing "destruct Z_le_gt_dec").
+ - Z.add has a new definition, hence, applying "simpl" on subterms of
+ its body might give different results than before.
+ - BigN.shiftl and BigN.shiftr have reversed arguments order, the
+ power function in BigN now takes two BigN.
+
+- Other changes in libraries:
+
+ - The definition of functions over "vectors" (list of fixed length)
+ have changed.
+ - TheoryList.v has been removed.
+
+- Slight changes in tactics:
+
+ - Less unfolding of fixpoints when applying destruct or inversion on
+ a fixpoint hiding an inductive type (add an extra call to simpl to
+ preserve compatibility).
+ - Less unexpected local definitions when applying "destruct"
+ (incompatibilities solvable by adapting name hypotheses).
+ - Tactic "apply" might succeed more often, e.g. by now solving
+ pattern-matching of the form ?f x y = g(x,y) (compatibility
+ ensured by using "Unset Tactic Pattern Unification"), but also
+ because it supports (full) betaiota (using "simple apply" might
+ then help).
+ - Tactic autorewrite does no longer instantiate pre-existing
+ existential variables.
+ - Tactic "info" is now available only for auto, eauto and trivial.
+
+- Miscellaneous changes:
+
+ - The command "Load" is now atomic for backtracking (use "Unset
+ Atomic Load" for compatibility).
diff --git a/INSTALL b/INSTALL
index 5ee00613..02c9eb9b 100644
--- a/INSTALL
+++ b/INSTALL
@@ -1,5 +1,5 @@
- INSTALLATION PROCEDURES FOR THE COQ V8.3 SYSTEM
+ INSTALLATION PROCEDURES FOR THE COQ V8.4 SYSTEM
-----------------------------------------------
diff --git a/INSTALL.macosx b/INSTALL.macosx
deleted file mode 100644
index cc1317b1..00000000
--- a/INSTALL.macosx
+++ /dev/null
@@ -1,20 +0,0 @@
-INSTALLATION PROCEDURE FOR THE PRECOMPILED COQ V8.1 SYSTEM UNDER MACOS X
-------------------------------------------------------------------------
-
-You can also use fink, or the MacOS X package prepared by the Coq
-team. To use the MacOS X package,:
-
-1) Download archive coq-8.1-macosx-ppc.dmg (for PowerPC-base computer)
- or coq-8.1-macosx-i386.dmg (for Pentium-based computer).
-
-2) Double-click on its icon; it mounts a disk volume named "Coq V8.1".
-
-3) Open volume "Coq 8.1" and double-click on coq-8.1.pkg to launch the
- installer (you'll need administrator permissions).
-
-4) Coq installs in /usr/local/bin, which should be in your PATH, and
- can be used from a Terminal window: the interactive toplevel is
- named coqtop and the compiler is coqc.
-
-If you have any trouble with this installation, please contact:
-coq-bugs@pauillac.inria.fr.
diff --git a/Makefile b/Makefile
index 0ff72856..bb5ec3bc 100644
--- a/Makefile
+++ b/Makefile
@@ -39,9 +39,13 @@
# File lists
###########################################################################
+# NB: due to limitations in Win32, please refrain using 'export' too much
+# to communicate between make sub-calls (in Win32, 8kb max per env variable,
+# 32kb total)
+
# !! Before using FIND_VCS_CLAUSE, please read how you should in the !!
# !! FIND_VCS_CLAUSE section of dev/doc/build-system.dev.txt !!
-export FIND_VCS_CLAUSE:='(' \
+FIND_VCS_CLAUSE:='(' \
-name '{arch}' -o \
-name '.svn' -o \
-name '_darcs' -o \
@@ -58,8 +62,8 @@ endef
## Files in the source tree
-export YACCFILES:=$(call find, '*.mly')
-export LEXFILES := $(call find, '*.mll')
+YACCFILES:=$(call find, '*.mly')
+LEXFILES := $(call find, '*.mll')
export MLLIBFILES := $(call find, '*.mllib')
export ML4FILES := $(call find, '*.ml4')
export CFILES := $(call find, '*.c')
@@ -73,13 +77,13 @@ EXISTINGMLI := $(call find, '*.mli')
## Files that will be generated
-export GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) \
+GENML4FILES:= $(ML4FILES:.ml4=.ml)
+GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) \
scripts/tolink.ml kernel/copcodes.ml
-export GENMLIFILES:=$(YACCFILES:.mly=.mli)
+GENMLIFILES:=$(YACCFILES:.mly=.mli)
+GENPLUGINSMOD:=$(filter plugins/%,$(MLLIBFILES:%.mllib=%_mod.ml))
export GENHFILES:=kernel/byterun/coq_jumptbl.h
export GENVFILES:=theories/Numbers/Natural/BigN/NMake_gen.v
-export GENPLUGINSMOD:=$(filter plugins/%,$(MLLIBFILES:%.mllib=%_mod.ml))
-export GENML4FILES:= $(ML4FILES:.ml4=.ml)
export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) $(GENVFILES) $(GENPLUGINSMOD)
# NB: all files in $(GENFILES) can be created initially, while
@@ -92,12 +96,9 @@ define diff
$(strip $(foreach f, $(1), $(if $(filter $(f),$(2)),,$f)))
endef
-export MLSTATICFILES := \
- $(call diff, $(EXISTINGML), $(GENMLFILES) $(GENML4FILES) $(GENPLUGINSMOD))
-export MLFILES := \
- $(sort $(EXISTINGML) $(GENMLFILES) $(GENML4FILES) $(GENPLUGINSMOD))
+export MLEXTRAFILES := $(GENMLFILES) $(GENML4FILES) $(GENPLUGINSMOD)
+export MLSTATICFILES := $(call diff, $(EXISTINGML), $(MLEXTRAFILES))
export MLIFILES := $(sort $(GENMLIFILES) $(EXISTINGMLI))
-export MLWITHOUTMLI := $(call diff, $(MLFILES), $(MLIFILES:.mli=.ml))
include Makefile.common
@@ -276,3 +277,14 @@ ifdef COQ_CONFIGURED
else
@echo "Please run ./configure first" >&2; exit 1
endif
+
+# Useful to check that the exported variables are within the win32 limits
+
+printenv:
+ @env
+ @echo
+ @echo -n "Maxsize (win32 limit is 8k) : "
+ @env | wc -L
+ @echo -n "Total (win32 limit is 32k) : "
+ @env | wc -m
+
diff --git a/Makefile.build b/Makefile.build
index 41dfabbf..fe99f3b0 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -36,10 +36,12 @@ endif
# of include, and they will then be automatically deleted, leading to an
# infinite loop.
-ALLDEPS=$(addsuffix .d, \
+MLFILES:=$(MLSTATICFILES) $(MLEXTRAFILES)
+
+ALLDEPS:=$(addsuffix .d, \
$(ML4FILES) $(MLFILES) $(MLIFILES) $(CFILES) $(MLLIBFILES) $(VFILES))
-.SECONDARY: $(ALLDEPS) $(GENFILES) $(GENML4FILES)
+.SECONDARY: $(ALLDEPS) $(GENFILES) $(ML4FILES:.ml4=.ml)
# NOTA: the -include below will lauch the build of all .d. Some of them
# will _fail_ at first, this is to be expected (no grammar.cma initially).
@@ -82,12 +84,15 @@ HIDE := $(if $(VERBOSE),,@)
LOCALINCLUDES=$(addprefix -I , $(SRCDIRS) )
MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
+COREMLINCLUDES=$(addprefix -I , $(CORESRCDIRS)) -I $(MYCAMLP4LIB)
OCAMLC += $(CAMLFLAGS)
OCAMLOPT += $(CAMLFLAGS)
BYTEFLAGS=$(MLINCLUDES) $(CAMLDEBUG) $(USERFLAGS)
OPTFLAGS=$(MLINCLUDES) $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS)
+COREBYTEFLAGS=$(COREMLINCLUDES) $(CAMLDEBUG) $(USERFLAGS)
+COREOPTFLAGS=$(COREMLINCLUDES) $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS)
DEPFLAGS= -slash $(LOCALINCLUDES)
define bestocaml
@@ -96,7 +101,7 @@ $(OCAMLOPT) $(OPTFLAGS) -o $@ $(1) $(addsuffix .cmxa,$(2)) $^ && $(STRIP) $@,\
$(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ $(1) $(addsuffix .cma,$(2)) $^)
endef
-CAMLP4DEPS=`sed -n -e 's@^(\*.*camlp4deps: "\(.*\)".*@\1@p' $<`
+CAMLP4DEPS=`LC_ALL=C sed -n -e 's@^(\*.*camlp4deps: "\(.*\)".*@\1@p' $<`
ifeq ($(CAMLP4),camlp5)
CAMLP4USE=pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION)
else
@@ -169,10 +174,12 @@ CINCLUDES= -I $(CAMLHLIB)
# libcoqrun.a, dllcoqrun.so
+# NB: We used to do a ranlib after ocamlmklib, but it seems that
+# ocamlmklib is already doing it
+
$(LIBCOQRUN): kernel/byterun/coq_jumptbl.h $(BYTERUN)
cd $(dir $(LIBCOQRUN)) && \
$(OCAMLMKLIB) -oc $(COQRUN) $(foreach u,$(BYTERUN),$(notdir $(u)))
- $(RANLIB) $(LIBCOQRUN)
#coq_jumptbl.h is required only if you have GCC 2.0 or later
kernel/byterun/coq_jumptbl.h : kernel/byterun/coq_instruct.h
@@ -201,12 +208,12 @@ states:: states/initial.coq
$(COQTOPOPT): $(BESTCOQMKTOP) $(LINKCMX) $(LIBCOQRUN)
$(SHOW)'COQMKTOP -o $@'
- $(HIDE)$(BESTCOQMKTOP) -boot -opt $(OPTFLAGS) -o $@
+ $(HIDE)$(BESTCOQMKTOP) -boot -opt $(COREOPTFLAGS) -o $@
$(STRIP) $@
$(COQTOPBYTE): $(BESTCOQMKTOP) $(LINKCMO) $(LIBCOQRUN)
$(SHOW)'COQMKTOP -o $@'
- $(HIDE)$(BESTCOQMKTOP) -boot -top $(BYTEFLAGS) -o $@
+ $(HIDE)$(BESTCOQMKTOP) -boot -top $(COREBYTEFLAGS) -o $@
$(COQTOPEXE): $(ORDER_ONLY_SEP) $(BESTCOQTOP)
cd bin; ln -sf coqtop.$(BEST)$(EXE) coqtop$(EXE)
@@ -544,9 +551,9 @@ $(FAKEIDE): lib/xml_lexer$(BESTOBJ) lib/xml_parser$(BESTOBJ) lib/xml_utils$(BEST
ifeq ($(CAMLP4),camlp4)
tools/compat5.cmo: tools/compat5.mlp
- $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp "$(CAMLP4O) -impl" -impl $<
+ $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) -impl' -impl $<
tools/compat5b.cmo: tools/compat5b.mlp
- $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp "$(CAMLP4O) -impl" -impl $<
+ $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) -impl' -impl $<
else
tools/compat5.cmo: tools/compat5.ml
$(OCAMLC) -c $<
@@ -729,7 +736,7 @@ dev/printers.cma: | dev/printers.mllib.d
parsing/grammar.cma: | parsing/grammar.mllib.d
$(SHOW)'Testing $@'
@touch test.ml4
- $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) -I $(CAMLLIB) $^ -impl" -impl test.ml4 -o test-grammar
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp '$(CAMLP4O) -I $(CAMLLIB) $^ -impl' -impl test.ml4 -o test-grammar
@rm -f test-grammar test.*
$(SHOW)'OCAMLC -a $@'
$(HIDE)$(OCAMLC) $(BYTEFLAGS) $^ -linkall -a -o $@
@@ -846,6 +853,12 @@ COND_OPTFLAGS= \
HACKMLI = $(if $(wildcard $)
+
+Theories:
+
+- Rendre transparent tous les theoremes prouvant {A}+{B}
+- Faire demarrer PolyList.nth a` l'indice 0
+ Renommer l'actuel nth en nth1 ??
+
+Doc:
+
+- Mettre jour les messages d'erreurs de Discriminate/Simplify_eq/Injection
+- Documenter le filtrage sur les types inductifs avec let-ins (dont la
+ compatibilite V6)
+
+- Ajouter let dans les rgles du CIC
+ -> FAIT, mais reste a documenter le let dans les inductifs
+ et les champs manifestes dans les Record
+- revoir le chapitre sur les tactiques utilisateur
+- faut-il mieux spcifier la smantique de Simpl (??)
+
+- Prciser la clarification syntaxique de IntroPattern
+- preciser que Goal vient en dernier dans une clause pattern list et
+ qu'il doit apparaitre si il y a un "in"
+
+- Omega Time debranche mais Omega System et Omega Action remarchent ?
+- Ajout "Replace in" (mais TODO)
+- Syntaxe Conditional tac Rewrite marche, documenter
+- Documenter Dependent Rewrite et CutRewrite ?
+- Ajouter les motifs sous-termes de ltac
+
+- ajouter doc de GenFixpoint (mais avant: changer syntaxe) (J. Forest ou Pierre C.)
+- mettre jour la doc de induction (arguments multiples) (Pierre C.)
+- mettre jour la doc de functional induction/scheme (J. Forest ou Pierre C.)
+--> mettre jour le CHANGES (vers la ligne 72)
+
+
diff --git a/checker/check.ml b/checker/check.ml
index bb42b949..237eb079 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* "
- echo "-with-ar "
- echo "-with-ranlib "
- printf "\tTells configure where to find gcc/ar/ranlib executables\n"
echo "-byte-only"
printf "\tCompiles only bytecode version of Coq\n"
echo "-debug"
@@ -119,10 +115,6 @@ best_compiler=opt
cflags="-fno-defer-pop -Wall -Wno-unused"
natdynlink=yes
-gcc_exec=gcc
-ar_exec=ar
-ranlib_exec=ranlib
-
local=false
coqrunbyteflags_spec=no
coqtoolsbyteflags_spec=no
@@ -254,18 +246,6 @@ while : ; do
no) with_geoproof=false;;
esac
shift;;
- -with-cc|-with-gcc|--with-cc|--with-gcc)
- gcc_spec=yes
- gcc_exec=$2
- shift;;
- -with-ar|--with-ar)
- ar_spec=yes
- ar_exec=$2
- shift;;
- -with-ranlib|--with-ranlib)
- ranlib_spec=yes
- ranlib_exec=$2
- shift;;
-makecmd|--makecmd) makecmd="$2"
shift;;
-byte-only|-byteonly|--byteonly|--byte-only) best_compiler=byte;;
@@ -292,17 +272,19 @@ case $DATEPGM in
"") echo "I can't find the program \"date\" in your path."
echo "Please give me the current date"
read COMPILEDATE;;
- *) COMPILEDATE=`LC_ALL=C LANG=C date +"%h %d %Y %H:%M:%S"`;;
+ *) COMPILEDATE=`LC_ALL=C LANG=C date +"%b %d %Y %H:%M:%S"`;;
esac
# Architecture
case $arch_spec in
no)
- # First we test if we are running a Cygwin system
+ # First we test if we are running a Cygwin or Mingw/Msys system
if [ `uname -s | cut -c -6` = "CYGWIN" ] ; then
ARCH="win32"
CYGWIN=yes
+ elif [ `uname -s | cut -c -7` = "MINGW32" ]; then
+ ARCH="win32"
else
# If not, we determine the architecture
if test -x /bin/uname ; then
@@ -437,12 +419,26 @@ if test ! -f "$CAMLC" ; then
exit 1
fi
-# Under Windows, OCaml only understands Windows filenames (C:\...)
-case $ARCH in
- win32) CAMLBIN=`cygpath -m ${CAMLBIN}`;;
+# Under Windows, we need to convert from cygwin/mingw paths (/c/Program Files/Ocaml)
+# to more windows-looking paths (c:/Program Files/Ocaml). Note that / are kept
+
+mk_win_path () {
+ case $ARCH,$CYGWIN in
+ win32,yes) cygpath -m "$1" ;;
+ win32*) "$ocamlexec" "tools/mingwpath.ml" "$1" ;;
+ *) echo "$1" ;;
+ esac
+}
+
+case $ARCH,$src_spec in
+ win32,yes) echo "Error: the -src option is currently not supported on Windows"
+ exit 1;;
+ win32) CAMLBIN=`mk_win_path "$CAMLBIN"`;;
esac
-CAMLVERSION=`"$bytecamlc" -version`
+# Beware of the final \r in Win32
+CAMLVERSION=`"$CAMLC" -version | tr -d "\r"`
+CAMLLIB=`"$CAMLC" -where | tr -d "\r"`
case $CAMLVERSION in
1.*|2.*|3.0*|3.10*|3.11.[01])
@@ -454,7 +450,7 @@ case $CAMLVERSION in
echo " Configuration script failed!"
exit 1
fi;;
- 3.11.2|3.12*)
+ 3.11.2|3.12*|4.*)
CAMLP4COMPAT="-loc loc"
echo "You have Objective-Caml $CAMLVERSION. Good!";;
*)
@@ -468,16 +464,9 @@ CAMLTAG=OCAML`echo $CAMLVERSION | sed -e "s/\([1-9]\)\.\([0-9]*\).*/\1\2/g"`
# For coqmktop & bytecode compiler
-case $ARCH in
- win32) # Awfull trick to get around a ^M problem at the end of CAMLLIB
- CAMLLIB=`"$CAMLC" -where | sed -e 's/^\(.*\)$/\1/'` ;;
- *)
- CAMLLIB=`"$CAMLC" -where`
-esac
-
if [ "$coq_debug_flag" = "-g" ]; then
case $CAMLTAG in
- OCAML31*)
+ OCAML31*|OCAML4*)
# Compilation debug flag
coq_debug_flag_opt="-g"
;;
@@ -485,7 +474,7 @@ if [ "$coq_debug_flag" = "-g" ]; then
fi
# Native dynlink
-if [ "$natdynlink" = "yes" -a -f `"$CAMLC" -where`/dynlink.cmxa ]; then
+if [ "$natdynlink" = "yes" -a -f "$CAMLLIB"/dynlink.cmxa ]; then
HASNATDYNLINK=true
else
HASNATDYNLINK=false
@@ -520,7 +509,8 @@ esac
# (this should become configurable some day)
CAMLP4BIN=${CAMLBIN}
-if [ "$usecamlp5" = "yes" ]; then
+case $usecamlp5 in
+ yes)
CAMLP4=camlp5
CAMLP4MOD=gramlib
if [ "$camlp5dir" != "" ]; then
@@ -539,38 +529,47 @@ if [ "$usecamlp5" = "yes" ]; then
CAMLP4LIB=+site-lib/camlp5
FULLCAMLP4LIB=${CAMLLIB}/site-lib/camlp5
else
- echo "Objective Caml $CAMLVERSION found but no Camlp5 installed."
- echo "Configuration script failed!"
- exit 1
+ echo "No Camlp5 installation found. Looking for Camlp4 instead..."
+ usecamlp5=no
fi
+esac
- camlp4oexec=`echo $camlp4oexec | sed -e 's/4/5/'`
- case `$camlp4oexec -v 2>&1` in
- *4.0*|*5.00*)
+# If we're (still...) going to use Camlp5, let's check its version
+
+case $usecamlp5 in
+ yes)
+ camlp4oexec=`echo "$camlp4oexec" | tr 4 5`
+ case `"$camlp4oexec" -v 2>&1` in
+ *"version 4.0"*|*5.00*)
echo "Camlp5 version < 5.01 not supported."
echo "Configuration script failed!"
exit 1;;
esac
+esac
+
+# We might now try to use Camlp4, either by explicit choice or
+# by lack of proper Camlp5 installation
-else # let's use camlp4
+case $usecamlp5 in
+ no)
CAMLP4=camlp4
CAMLP4MOD=camlp4lib
CAMLP4LIB=+camlp4
FULLCAMLP4LIB=${CAMLLIB}/camlp4
if [ ! -f "${FULLCAMLP4LIB}/${CAMLP4MOD}.cma" ]; then
- echo "Objective Caml $CAMLVERSION found but no Camlp4 installed."
+ echo "No Camlp4 installation found."
echo "Configuration script failed!"
exit 1
fi
camlp4oexec=${camlp4oexec}rf
- if [ "`$camlp4oexec 2>&1`" != "" ]; then
+ if [ "`"$camlp4oexec" 2>&1`" != "" ]; then
echo "Error: $camlp4oexec not found or not executable."
echo "Configuration script failed!"
exit 1
fi
-fi
+esac
# do we have a native compiler: test of ocamlopt and its version
@@ -595,18 +594,17 @@ fi
# OS dependent libraries
-case $ARCH in
+OSDEPLIBS="-cclib -lunix"
+case $ARCH,$CYGWIN in
sun4*) OS=`uname -r`
case $OS in
5*) OS="Sun Solaris $OS"
- OSDEPLIBS="-cclib -lunix -cclib -lnsl -cclib -lsocket";;
+ OSDEPLIBS="$OSDEPLIBS -cclib -lnsl -cclib -lsocket";;
*) OS="Sun OS $OS"
- OSDEPLIBS="-cclib -lunix"
esac;;
- win32) OS="Win32"
- OSDEPLIBS="-cclib -lunix"
+ win32,yes) OS="Win32 (Cygwin)"
cflags="-mno-cygwin $cflags";;
- *) OSDEPLIBS="-cclib -lunix"
+ win32,*) OS="Win32 (MinGW)";;
esac
# lablgtk2 and CoqIDE
@@ -628,11 +626,11 @@ if [ "$coqide_spec" = "yes" -a "$COQIDE" = "no" ]; then
echo "CoqIde disabled as requested."
else
case $lablgtkdir_spec in
- no)
- if [ -f "${CAMLLIB}/lablgtk2/glib.mli" ]; then
+ no)
+ if lablgtkdir=$(ocamlfind query lablgtk2 2> /dev/null); then
+ lablgtkdir_spec=yes
+ elif [ -f "${CAMLLIB}/lablgtk2/glib.mli" ]; then
lablgtkdir=${CAMLLIB}/lablgtk2
- elif [ -f "${CAMLLIB}/site-lib/lablgtk2/glib.mli" ]; then
- lablgtkdir=${CAMLLIB}/site-lib/lablgtk2
fi;;
yes)
if [ ! -f "$lablgtkdir/glib.mli" ]; then
@@ -656,10 +654,10 @@ else
else
echo "LablGtk2 found, native threads: native CoqIde will be available."
COQIDE=opt
- if [ "$nomacintegration_spec" = "no" ] && pkg-config --exists ige-mac-integration;
+ if [ "$nomacintegration_spec" = "no" ] && pkg-config --exists gtk-mac-integration;
then
- cflags=$cflags" `pkg-config --cflags ige-mac-integration`"
- IDEARCHFLAGS='-ccopt "`pkg-config --libs ige-mac-integration`"'
+ cflags=$cflags" `pkg-config --cflags gtk-mac-integration`"
+ IDEARCHFLAGS='-ccopt "`pkg-config --libs gtk-mac-integration`"'
IDEARCHFILE=ide/ide_mac_stubs.o
IDEARCHDEF=QUARTZ
elif [ "$ARCH" = "win32" ];
@@ -685,9 +683,6 @@ esac
# strip command
case $ARCH in
- win32)
- # true -> strip : it exists under cygwin !
- STRIPCOMMAND="strip";;
Darwin) if [ "$HASNATDYNLINK" = "true" ]
then
STRIPCOMMAND="true"
@@ -703,13 +698,6 @@ case $ARCH in
fi
esac
-# mktexlsr
-#MKTEXLSR=`which mktexlsr`
-#case $MKTEXLSR in
-# "") MKTEXLSR=true;;
-#esac
-
-# "
### Test if documentation can be compiled (latex, hevea)
if test "$with_doc" = "all"
@@ -727,26 +715,28 @@ fi
###########################################
# bindir, libdir, mandir, docdir, etc.
-case $src_spec in
- no) COQTOP=${COQSRC}
-esac
-
# OCaml only understand Windows filenames (C:\...)
case $ARCH in
- win32) COQTOP=`cygpath -m ${COQTOP}`
+ win32) COQSRC=`mk_win_path "$COQSRC"`
+ CAMLBIN=`mk_win_path "$CAMLBIN"`
+ CAMLP4BIN=`mk_win_path "$CAMLP4BIN"`
+esac
+
+case $src_spec in
+ no) COQTOP=${COQSRC}
esac
case $ARCH$CYGWIN in
win32)
- W32PREF='C:\\coq\\'
- bindir_def=${W32PREF}bin
- libdir_def=${W32PREF}lib
- configdir_def=${W32PREF}config
- datadir_def=${W32PREF}share
- mandir_def=${W32PREF}man
- docdir_def=${W32PREF}doc
- emacslib_def=${W32PREF}emacs
- coqdocdir_def=${W32PREF}latex;;
+ W32PREF='C:\coq\'
+ bindir_def="${W32PREF}bin"
+ libdir_def="${W32PREF}lib"
+ configdir_def="${W32PREF}config"
+ datadir_def="${W32PREF}share"
+ mandir_def="${W32PREF}man"
+ docdir_def="${W32PREF}doc"
+ emacslib_def="${W32PREF}emacs"
+ coqdocdir_def="${W32PREF}latex";;
*)
bindir_def=/usr/local/bin
libdir_def=/usr/local/lib/coq
@@ -755,7 +745,7 @@ case $ARCH$CYGWIN in
mandir_def=/usr/local/share/man
docdir_def=/usr/local/share/doc/coq
emacslib_def=/usr/local/share/emacs/site-lisp
- coqdocdir_def=/usr/local/share/texmf/tex/latex/misc;;
+ coqdocdir_def=/usr/local/share/texmf/tex/latex/misc;;
esac
emacs_def=emacs
@@ -764,7 +754,7 @@ case $bindir_spec/$prefix_spec/$local in
yes/*/*) BINDIR=$bindir ;;
*/yes/*) BINDIR=$prefix/bin ;;
*/*/true) BINDIR=$COQTOP/bin ;;
- *) printf "Where should I install the Coq binaries [$bindir_def]? "
+ *) printf "Where should I install the Coq binaries [%s]? " "$bindir_def"
read BINDIR
case $BINDIR in
"") BINDIR=$bindir_def;;
@@ -781,7 +771,7 @@ case $libdir_spec/$prefix_spec/$local in
*) LIBDIR=$prefix/lib/coq ;;
esac ;;
*/*/true) LIBDIR=$COQTOP ;;
- *) printf "Where should I install the Coq library [$libdir_def]? "
+ *) printf "Where should I install the Coq library [%s]? " "$libdir_def"
read LIBDIR
libdir_spec=yes
case $LIBDIR in
@@ -790,11 +780,6 @@ case $libdir_spec/$prefix_spec/$local in
esac;;
esac
-case $libdir_spec in
- yes) LIBDIR_OPTION="Some \"$LIBDIR\"";;
- *) LIBDIR_OPTION="None";;
-esac
-
case $configdir_spec/$prefix_spec/$local in
yes/*/*) CONFIGDIR=$configdir;;
*/yes/*) configdir_spec=yes
@@ -804,7 +789,7 @@ case $configdir_spec/$prefix_spec/$local in
esac;;
*/*/true) CONFIGDIR=$COQTOP/ide
configdir_spec=yes;;
- *) printf "Where should I install the Coqide configuration files [$configdir_def]? "
+ *) printf "Where should I install the Coqide configuration files [%s]? " "$configdir_def"
read CONFIGDIR
case $CONFIGDIR in
"") CONFIGDIR=$configdir_def;;
@@ -812,17 +797,12 @@ case $configdir_spec/$prefix_spec/$local in
esac;;
esac
-case $configdir_spec in
- yes) CONFIGDIR_OPTION="Some \"$CONFIGDIR\"";;
- *) CONFIGDIR_OPTION="None";;
-esac
-
case $datadir_spec/$prefix_spec/$local in
yes/*/*) DATADIR=$datadir;;
*/yes/*) DATADIR=$prefix/share/coq;;
*/*/true) DATADIR=$COQTOP/ide
datadir_spec=yes;;
- *) printf "Where should I install the Coqide data files [$datadir_def]? "
+ *) printf "Where should I install the Coqide data files [%s]? " "$datadir_def"
read DATADIR
case $DATADIR in
"") DATADIR=$datadir_def;;
@@ -830,17 +810,11 @@ case $datadir_spec/$prefix_spec/$local in
esac;;
esac
-case $datadir_spec in
- yes) DATADIR_OPTION="Some \"$DATADIR\"";;
- *) DATADIR_OPTION="None";;
-esac
-
-
case $mandir_spec/$prefix_spec/$local in
yes/*/*) MANDIR=$mandir;;
*/yes/*) MANDIR=$prefix/share/man ;;
*/*/true) MANDIR=$COQTOP/man ;;
- *) printf "Where should I install the Coq man pages [$mandir_def]? "
+ *) printf "Where should I install the Coq man pages [%s]? " "$mandir_def"
read MANDIR
case $MANDIR in
"") MANDIR=$mandir_def;;
@@ -852,7 +826,7 @@ case $docdir_spec/$prefix_spec/$local in
yes/*/*) DOCDIR=$docdir;;
*/yes/*) DOCDIR=$prefix/share/doc/coq;;
*/*/true) DOCDIR=$COQTOP/doc;;
- *) printf "Where should I install the Coq documentation [$docdir_def]? "
+ *) printf "Where should I install the Coq documentation [%s]? " "$docdir_def"
read DOCDIR
case $DOCDIR in
"") DOCDIR=$docdir_def;;
@@ -868,7 +842,7 @@ case $emacslib_spec/$prefix_spec/$local in
*) EMACSLIB=$prefix/share/emacs/site-lisp ;;
esac ;;
*/*/true) EMACSLIB=$COQTOP/tools/emacs ;;
- *) printf "Where should I install the Coq Emacs mode [$emacslib_def]? "
+ *) printf "Where should I install the Coq Emacs mode [%s]? " "$emacslib_def"
read EMACSLIB
case $EMACSLIB in
"") EMACSLIB=$emacslib_def;;
@@ -884,7 +858,7 @@ case $coqdocdir_spec/$prefix_spec/$local in
*) COQDOCDIR=$prefix/share/emacs/site-lisp ;;
esac ;;
*/*/true) COQDOCDIR=$COQTOP/tools/coqdoc ;;
- *) printf "Where should I install Coqdoc TeX/LaTeX files [$coqdocdir_def]? "
+ *) printf "Where should I install Coqdoc TeX/LaTeX files [%s]? " "$coqdocdir_def"
read COQDOCDIR
case $COQDOCDIR in
"") COQDOCDIR=$coqdocdir_def;;
@@ -914,14 +888,14 @@ case $coqtoolsbyteflags_spec/$custom_spec/$CUSTOM_OS in
esac
# case $emacs_spec in
-# no) printf "Which Emacs command should I use to compile coq.el [$emacs_def]? "
+# no) printf "Which Emacs command should I use to compile coq.el [%s]? " "$emacs_def"
# read EMACS
# case $EMACS in
-# "") EMACS=$emacs_def;;
+# "") EMACS="$emacs_def";;
# *) true;;
# esac;;
-# yes) EMACS=$emacs;;
+# yes) EMACS="$emacs";;
# esac
@@ -1016,51 +990,63 @@ config_template="$COQSRC/config/Makefile.template"
### After this line, be careful when using variables,
### since some of them (e.g. $COQSRC) will be escaped
-
-# An escaped version of a variable
-escape_var () {
-"$ocamlexec" 2>&1 1>/dev/null < "$config_file"
+cat << END_OF_MAKEFILE > $config_file
+###### config/Makefile : Configuration file for Coq ##############
+# #
+# This file is generated by the script "configure" #
+# DO NOT EDIT IT !! DO NOT EDIT IT !! DO NOT EDIT IT !! #
+# If something is wrong below, then rerun the script "configure" #
+# with the good options (see the file INSTALL). #
+# #
+##################################################################
+
+#Variable used to detect whether ./configure has run successfully.
+COQ_CONFIGURED=yes
+
+# Local use (no installation)
+LOCAL=$local
+
+# Bytecode link flags for VM ("-custom" or "-dllib -lcoqrun")
+COQRUNBYTEFLAGS=$COQRUNBYTEFLAGS
+COQTOOLSBYTEFLAGS=$COQTOOLSBYTEFLAGS
+$BUILDLDPATH
+
+# Paths for true installation
+# BINDIR=path where coqtop, coqc, coqmktop, coq-tex, coqdep, gallina and
+# do_Makefile will reside
+# LIBDIR=path where the Coq library will reside
+# MANDIR=path where to install manual pages
+# EMACSDIR=path where to put Coq's Emacs mode (coq.el)
+BINDIR="$BINDIR"
+COQLIBINSTALL="$LIBDIR"
+CONFIGDIR="$CONFIGDIR"
+DATADIR="$DATADIR"
+MANDIR="$MANDIR"
+DOCDIR="$DOCDIR"
+EMACSLIB="$EMACSLIB"
+EMACS=$EMACS
+
+# Path to Coq distribution
+COQSRC="$COQSRC"
+VERSION=$VERSION
+
+# Ocaml version number
+CAMLVERSION=$CAMLTAG
+
+# Ocaml libraries
+CAMLLIB="$CAMLLIB"
+
+# Ocaml .h directory
+CAMLHLIB="$CAMLLIB"
+
+# Camlp4 : flavor, binaries, libraries ...
+# NB : CAMLP4BIN can be empty if camlp4 is in the PATH
+# NB : avoid using CAMLP4LIB (conflict under Windows)
+CAMLP4BIN="$CAMLP4BIN"
+CAMLP4=$CAMLP4
+CAMLP4O=$camlp4oexec
+CAMLP4COMPAT=$CAMLP4COMPAT
+MYCAMLP4LIB="$CAMLP4LIB"
+
+# LablGTK
+COQIDEINCLUDES=$LABLGTKINCLUDES
+
+# Objective-Caml compile command
+OCAML="$ocamlexec"
+OCAMLC="$bytecamlc"
+OCAMLMKLIB="$ocamlmklibexec"
+OCAMLOPT="$nativecamlc"
+OCAMLDEP="$ocamldepexec"
+OCAMLDOC="$ocamldocexec"
+OCAMLLEX="$ocamllexexec"
+OCAMLYACC="$ocamlyaccexec"
+
+# Caml link command and Caml make top command
+CAMLLINK="$bytecamlc"
+CAMLOPTLINK="$nativecamlc"
+CAMLMKTOP="$ocamlmktopexec"
+
+# Caml flags
+CAMLFLAGS=-rectypes $coq_annotate_flag
+
+# Compilation debug flags
+CAMLDEBUG=$coq_debug_flag
+CAMLDEBUGOPT=$coq_debug_flag_opt
+
+# User compilation flag
+USERFLAGS=
+
+# Flags for GCC
+CFLAGS=$cflags
+
+# Compilation profile flag
+CAMLTIMEPROF=$coq_profile_flag
+
+# The best compiler: native (=opt) or bytecode (=byte) if no native compiler
+BEST=$best_compiler
+
+# Your architecture
+# Can be obtain by UNIX command arch
+ARCH=$ARCH
+HASNATDYNLINK=$NATDYNLINKFLAG
+
+# Supplementary libs for some systems, currently:
+# . Sun Solaris: -cclib -lunix -cclib -lnsl -cclib -lsocket
+# . others : -cclib -lunix
+OSDEPLIBS=$OSDEPLIBS
+
+# executable files extension, currently:
+# Unix systems:
+# Win32 systems : .exe
+EXE=$EXE
+DLLEXT=$DLLEXT
+
+# the command MKDIR (try to replace it with mkdirhier if you have problems)
+MKDIR=mkdir -p
+
+# where to put the coqdoc.sty style file
+COQDOCDIR="$COQDOCDIR"
+
+#the command STRIP
+# Unix systems and profiling: true
+# Unix systems and no profiling: strip
+STRIP=$STRIPCOMMAND
+
+# CoqIde (no/byte/opt)
+HASCOQIDE=$COQIDE
+IDEOPTFLAGS=$IDEARCHFLAGS
+IDEOPTDEPS=$IDEARCHFILE
+IDEOPTINT=$IDEARCHDEF
+
+# Defining REVISION
+CHECKEDOUT=$checkedout
+
+# Option to control compilation and installation of the documentation
+WITHDOC=$with_doc
+
+# make or sed are bogus and believe lines not terminating by a return
+# are inexistent
+END_OF_MAKEFILE
chmod a-w "$config_file"
diff --git a/dev/db_printers.ml b/dev/db_printers.ml
index b3edd7d0..f54df8a8 100644
--- a/dev/db_printers.ml
+++ b/dev/db_printers.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* \(.*\)$/\1\2/
+s/^;\{0,1\} *\(.*\)\(.*\)$/\1\2/
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 3116cbf2..0038e78a 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* try pp(pr_ltype x) with e -> pp (str (Printexc.to_string
let ppfconstr c = ppconstr (Closure.term_of_fconstr c)
-let ppbigint n = pp (Bigint.pr_bigint n);;
+let ppbigint n = pp (str (Bigint.to_string n));;
let prset pr l = str "[" ++ hov 0 (prlist_with_sep spc pr l) ++ str "]"
let ppintset l = pp (prset int (Intset.elements l))
diff --git a/doc/refman/RefMan-sch.tex b/doc/refman/RefMan-sch.tex
deleted file mode 100644
index 707ee824..00000000
--- a/doc/refman/RefMan-sch.tex
+++ /dev/null
@@ -1,418 +0,0 @@
-\chapter{Proof schemes}
-
-\section{Generation of induction principles with {\tt Scheme}}
-\label{Scheme}
-\index{Schemes}
-\comindex{Scheme}
-
-The {\tt Scheme} command is a high-level tool for generating
-automatically (possibly mutual) induction principles for given types
-and sorts. Its syntax follows the schema:
-\begin{quote}
-{\tt Scheme {\ident$_1$} := Induction for \ident'$_1$ Sort {\sort$_1$} \\
- with\\
- \mbox{}\hspace{0.1cm} \dots\\
- with {\ident$_m$} := Induction for {\ident'$_m$} Sort
- {\sort$_m$}}
-\end{quote}
-where \ident'$_1$ \dots\ \ident'$_m$ are different inductive type
-identifiers belonging to the same package of mutual inductive
-definitions. This command generates {\ident$_1$}\dots{} {\ident$_m$}
-to be mutually recursive definitions. Each term {\ident$_i$} proves a
-general principle of mutual induction for objects in type {\term$_i$}.
-
-\begin{Variants}
-\item {\tt Scheme {\ident$_1$} := Minimality for \ident'$_1$ Sort {\sort$_1$} \\
- with\\
- \mbox{}\hspace{0.1cm} \dots\ \\
- with {\ident$_m$} := Minimality for {\ident'$_m$} Sort
- {\sort$_m$}}
-
- Same as before but defines a non-dependent elimination principle more
- natural in case of inductively defined relations.
-
-\item {\tt Scheme Equality for \ident$_1$\comindex{Scheme Equality}}
-
- Tries to generate a boolean equality and a proof of the
- decidability of the usual equality. If \ident$_i$ involves
- some other inductive types, their equality has to be defined first.
-
-\item {\tt Scheme Induction for \ident$_1$ Sort {\sort$_1$} \\
- with\\
- \mbox{}\hspace{0.1cm} \dots\\
- with Induction for {\ident$_m$} Sort
- {\sort$_m$}}
-
- If you do not provide the name of the schemes, they will be automatically
- computed from the sorts involved (works also with Minimality).
-
-\end{Variants}
-\label{Scheme-examples}
-
-\firstexample
-\example{Induction scheme for \texttt{tree} and \texttt{forest}}
-
-The definition of principle of mutual induction for {\tt tree} and
-{\tt forest} over the sort {\tt Set} is defined by the command:
-
-\begin{coq_eval}
-Reset Initial.
-Variables A B : Set.
-\end{coq_eval}
-
-\begin{coq_example*}
-Inductive tree : Set :=
- node : A -> forest -> tree
-with forest : Set :=
- | leaf : B -> forest
- | cons : tree -> forest -> forest.
-
-Scheme tree_forest_rec := Induction for tree Sort Set
- with forest_tree_rec := Induction for forest Sort Set.
-\end{coq_example*}
-
-You may now look at the type of {\tt tree\_forest\_rec}:
-
-\begin{coq_example}
-Check tree_forest_rec.
-\end{coq_example}
-
-This principle involves two different predicates for {\tt trees} and
-{\tt forests}; it also has three premises each one corresponding to a
-constructor of one of the inductive definitions.
-
-The principle {\tt forest\_tree\_rec} shares exactly the same
-premises, only the conclusion now refers to the property of forests.
-
-\begin{coq_example}
-Check forest_tree_rec.
-\end{coq_example}
-
-\example{Predicates {\tt odd} and {\tt even} on naturals}
-
-Let {\tt odd} and {\tt even} be inductively defined as:
-
-% Reset Initial.
-\begin{coq_eval}
-Open Scope nat_scope.
-\end{coq_eval}
-
-\begin{coq_example*}
-Inductive odd : nat -> Prop :=
- oddS : forall n:nat, even n -> odd (S n)
-with even : nat -> Prop :=
- | evenO : even 0
- | evenS : forall n:nat, odd n -> even (S n).
-\end{coq_example*}
-
-The following command generates a powerful elimination
-principle:
-
-\begin{coq_example}
-Scheme odd_even := Minimality for odd Sort Prop
- with even_odd := Minimality for even Sort Prop.
-\end{coq_example}
-
-The type of {\tt odd\_even} for instance will be:
-
-\begin{coq_example}
-Check odd_even.
-\end{coq_example}
-
-The type of {\tt even\_odd} shares the same premises but the
-conclusion is {\tt (n:nat)(even n)->(Q n)}.
-
-\subsection{Automatic declaration of schemes}
-\comindex{Set Equality Schemes}
-\comindex{Set Elimination Schemes}
-
-It is possible to deactivate the automatic declaration of the induction
- principles when defining a new inductive type with the
- {\tt Unset Elimination Schemes} command. It may be
-reactivated at any time with {\tt Set Elimination Schemes}.
-\\
-
-You can also activate the automatic declaration of those boolean equalities
-(see the second variant of {\tt Scheme}) with the {\tt Set Equality Schemes}
- command. However you have to be careful with this option since
-\Coq~ may now reject well-defined inductive types because it cannot compute
-a boolean equality for them.
-
-\subsection{\tt Combined Scheme}
-\label{CombinedScheme}
-\comindex{Combined Scheme}
-
-The {\tt Combined Scheme} command is a tool for combining
-induction principles generated by the {\tt Scheme} command.
-Its syntax follows the schema :
-\begin{quote}
-{\tt Combined Scheme {\ident$_0$} from {\ident$_1$}, .., {\ident$_n$}}
-\end{quote}
-where
-\ident$_1$ \ldots \ident$_n$ are different inductive principles that must belong to
-the same package of mutual inductive principle definitions. This command
-generates {\ident$_0$} to be the conjunction of the principles: it is
-built from the common premises of the principles and concluded by the
-conjunction of their conclusions.
-
-\Example
-We can define the induction principles for trees and forests using:
-\begin{coq_example}
-Scheme tree_forest_ind := Induction for tree Sort Prop
- with forest_tree_ind := Induction for forest Sort Prop.
-\end{coq_example}
-
-Then we can build the combined induction principle which gives the
-conjunction of the conclusions of each individual principle:
-\begin{coq_example}
-Combined Scheme tree_forest_mutind from tree_forest_ind, forest_tree_ind.
-\end{coq_example}
-
-The type of {\tt tree\_forest\_mutrec} will be:
-\begin{coq_example}
-Check tree_forest_mutind.
-\end{coq_example}
-
-\section{Generation of induction principles with {\tt Functional Scheme}}
-\label{FunScheme}
-\comindex{Functional Scheme}
-
-The {\tt Functional Scheme} command is a high-level experimental
-tool for generating automatically induction principles
-corresponding to (possibly mutually recursive) functions. Its
-syntax follows the schema:
-\begin{quote}
-{\tt Functional Scheme {\ident$_1$} := Induction for \ident'$_1$ Sort {\sort$_1$} \\
- with\\
- \mbox{}\hspace{0.1cm} \dots\ \\
- with {\ident$_m$} := Induction for {\ident'$_m$} Sort
- {\sort$_m$}}
-\end{quote}
-where \ident'$_1$ \dots\ \ident'$_m$ are different mutually defined function
-names (they must be in the same order as when they were defined).
-This command generates the induction principles
-\ident$_1$\dots\ident$_m$, following the recursive structure and case
-analyses of the functions \ident'$_1$ \dots\ \ident'$_m$.
-
-\Rem
-There is a difference between obtaining an induction scheme by using
-\texttt{Functional Scheme} on a function defined by \texttt{Function}
-or not. Indeed \texttt{Function} generally produces smaller
-principles, closer to the definition written by the user.
-
-\firstexample
-\example{Induction scheme for \texttt{div2}}
-\label{FunScheme-examples}
-
-We define the function \texttt{div2} as follows:
-
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-
-\begin{coq_example*}
-Require Import Arith.
-Fixpoint div2 (n:nat) : nat :=
- match n with
- | O => 0
- | S O => 0
- | S (S n') => S (div2 n')
- end.
-\end{coq_example*}
-
-The definition of a principle of induction corresponding to the
-recursive structure of \texttt{div2} is defined by the command:
-
-\begin{coq_example}
-Functional Scheme div2_ind := Induction for div2 Sort Prop.
-\end{coq_example}
-
-You may now look at the type of {\tt div2\_ind}:
-
-\begin{coq_example}
-Check div2_ind.
-\end{coq_example}
-
-We can now prove the following lemma using this principle:
-
-\begin{coq_example*}
-Lemma div2_le' : forall n:nat, div2 n <= n.
-intro n.
- pattern n , (div2 n).
-\end{coq_example*}
-
-\begin{coq_example}
-apply div2_ind; intros.
-\end{coq_example}
-
-\begin{coq_example*}
-auto with arith.
-auto with arith.
-simpl; auto with arith.
-Qed.
-\end{coq_example*}
-
-We can use directly the \texttt{functional induction}
-(\ref{FunInduction}) tactic instead of the pattern/apply trick:
-\tacindex{functional induction}
-
-\begin{coq_example*}
-Reset div2_le'.
-Lemma div2_le : forall n:nat, div2 n <= n.
-intro n.
-\end{coq_example*}
-
-\begin{coq_example}
-functional induction (div2 n).
-\end{coq_example}
-
-\begin{coq_example*}
-auto with arith.
-auto with arith.
-auto with arith.
-Qed.
-\end{coq_example*}
-
-\Rem There is a difference between obtaining an induction scheme for a
-function by using \texttt{Function} (see Section~\ref{Function}) and by
-using \texttt{Functional Scheme} after a normal definition using
-\texttt{Fixpoint} or \texttt{Definition}. See \ref{Function} for
-details.
-
-
-\example{Induction scheme for \texttt{tree\_size}}
-
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-
-We define trees by the following mutual inductive type:
-
-\begin{coq_example*}
-Variable A : Set.
-Inductive tree : Set :=
- node : A -> forest -> tree
-with forest : Set :=
- | empty : forest
- | cons : tree -> forest -> forest.
-\end{coq_example*}
-
-We define the function \texttt{tree\_size} that computes the size
-of a tree or a forest. Note that we use \texttt{Function} which
-generally produces better principles.
-
-\begin{coq_example*}
-Function tree_size (t:tree) : nat :=
- match t with
- | node A f => S (forest_size f)
- end
- with forest_size (f:forest) : nat :=
- match f with
- | empty => 0
- | cons t f' => (tree_size t + forest_size f')
- end.
-\end{coq_example*}
-
-\Rem \texttt{Function} generates itself non mutual induction
-principles {\tt tree\_size\_ind} and {\tt forest\_size\_ind}:
-
-\begin{coq_example}
-Check tree_size_ind.
-\end{coq_example}
-
-The definition of mutual induction principles following the recursive
-structure of \texttt{tree\_size} and \texttt{forest\_size} is defined
-by the command:
-
-\begin{coq_example*}
-Functional Scheme tree_size_ind2 := Induction for tree_size Sort Prop
-with forest_size_ind2 := Induction for forest_size Sort Prop.
-\end{coq_example*}
-
-You may now look at the type of {\tt tree\_size\_ind2}:
-
-\begin{coq_example}
-Check tree_size_ind2.
-\end{coq_example}
-
-\section{Generation of inversion principles with \tt Derive Inversion}
-\label{Derive-Inversion}
-\comindex{Derive Inversion}
-
-The syntax of {\tt Derive Inversion} follows the schema:
-\begin{quote}
-{\tt Derive Inversion {\ident} with forall
- $(\vec{x} : \vec{T})$, $I~\vec{t}$ Sort \sort}
-\end{quote}
-
-This command generates an inversion principle for the
-\texttt{inversion \dots\ using} tactic.
-\tacindex{inversion \dots\ using}
-Let $I$ be an inductive predicate and $\vec{x}$ the variables
-occurring in $\vec{t}$. This command generates and stocks the
-inversion lemma for the sort \sort~ corresponding to the instance
-$\forall (\vec{x}:\vec{T}), I~\vec{t}$ with the name {\ident} in the {\bf
-global} environment. When applied, it is equivalent to having inverted
-the instance with the tactic {\tt inversion}.
-
-\begin{Variants}
-\item \texttt{Derive Inversion\_clear {\ident} with forall
- $(\vec{x}:\vec{T})$, $I~\vec{t}$ Sort \sort}\\
- \comindex{Derive Inversion\_clear}
- When applied, it is equivalent to having
- inverted the instance with the tactic \texttt{inversion}
- replaced by the tactic \texttt{inversion\_clear}.
-\item \texttt{Derive Dependent Inversion {\ident} with forall
- $(\vec{x}:\vec{T})$, $I~\vec{t}$ Sort \sort}\\
- \comindex{Derive Dependent Inversion}
- When applied, it is equivalent to having
- inverted the instance with the tactic \texttt{dependent inversion}.
-\item \texttt{Derive Dependent Inversion\_clear {\ident} with forall
- $(\vec{x}:\vec{T})$, $I~\vec{t}$ Sort \sort}\\
- \comindex{Derive Dependent Inversion\_clear}
- When applied, it is equivalent to having
- inverted the instance with the tactic \texttt{dependent inversion\_clear}.
-\end{Variants}
-
-\Example
-
-Let us consider the relation \texttt{Le} over natural numbers and the
-following variable:
-
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-
-\begin{coq_example*}
-Inductive Le : nat -> nat -> Set :=
- | LeO : forall n:nat, Le 0 n
- | LeS : forall n m:nat, Le n m -> Le (S n) (S m).
-Variable P : nat -> nat -> Prop.
-\end{coq_example*}
-
-To generate the inversion lemma for the instance
-\texttt{(Le (S n) m)} and the sort \texttt{Prop}, we do:
-
-\begin{coq_example*}
-Derive Inversion_clear leminv with (forall n m:nat, Le (S n) m) Sort Prop.
-\end{coq_example*}
-
-\begin{coq_example}
-Check leminv.
-\end{coq_example}
-
-Then we can use the proven inversion lemma:
-
-\begin{coq_eval}
-Lemma ex : forall n m:nat, Le (S n) m -> P n m.
-intros.
-\end{coq_eval}
-
-\begin{coq_example}
-Show.
-\end{coq_example}
-
-\begin{coq_example}
-inversion H using leminv.
-\end{coq_example}
-
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 0ee101c8..833b5c4c 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -400,6 +400,7 @@ through the Require Import command.
theories/Lists/List.v
theories/Lists/ListSet.v
theories/Lists/SetoidList.v
+ theories/Lists/SetoidPermutation.v
theories/Lists/Streams.v
theories/Lists/StreamMemo.v
theories/Lists/ListTactics.v
@@ -523,7 +524,10 @@ through the Require Import command.
theories/Reals/Rsigma.v
theories/Reals/R_sqr.v
theories/Reals/Rtrigo_fun.v
+ theories/Reals/Rtrigo1.v
theories/Reals/Rtrigo.v
+ theories/Reals/Ratan.v
+ theories/Reals/Machin.v
theories/Reals/SplitAbsolu.v
theories/Reals/SplitRmult.v
theories/Reals/Alembert.v
@@ -544,6 +548,8 @@ through the Require Import command.
theories/Reals/Ranalysis2.v
theories/Reals/Ranalysis3.v
theories/Reals/Ranalysis4.v
+ theories/Reals/Ranalysis5.v
+ theories/Reals/Ranalysis_reg.v
theories/Reals/Rcomplete.v
theories/Reals/RiemannInt.v
theories/Reals/RiemannInt_SF.v
diff --git a/ide/command_windows.ml b/ide/command_windows.ml
index a34e5ebe..470bd5b4 100644
--- a/ide/command_windows.ml
+++ b/ide/command_windows.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(*
let path = match status.Interface.status_path with
- | None -> ""
- | Some p -> " in " ^ p
+ | [] | _ :: [] -> "" (* Drop the topmost level, usually "Top" *)
+ | _ :: l -> " in " ^ String.concat "." l
in
let name = match status.Interface.status_proofname with
| None -> ""
@@ -2449,13 +2449,13 @@ let main files =
try configure ~apply:update_notebook_pos ()
with _ -> flash_info "Cannot save preferences"
end;
- reset_revert_timer ()) ~stock:`PREFERENCES;
+ reset_revert_timer ()) ~accel:"," ~stock:`PREFERENCES;
(* GAction.add_action "Save preferences" ~label:"_Save preferences" ~callback:(fun _ -> save_pref ()); *) ];
GAction.add_actions view_actions [
GAction.add_action "View" ~label:"_View";
- GAction.add_action "Previous tab" ~label:"_Previous tab" ~accel:("Left") ~stock:`GO_BACK
+ GAction.add_action "Previous tab" ~label:"_Previous tab" ~accel:("Left") ~stock:`GO_BACK
~callback:(fun _ -> session_notebook#previous_page ());
- GAction.add_action "Next tab" ~label:"_Next tab" ~accel:("Right") ~stock:`GO_FORWARD
+ GAction.add_action "Next tab" ~label:"_Next tab" ~accel:("Right") ~stock:`GO_FORWARD
~callback:(fun _ -> session_notebook#next_page ());
GAction.add_toggle_action "Show Toolbar" ~label:"Show _Toolbar"
~active:(!current.show_toolbar) ~callback:
@@ -2624,6 +2624,7 @@ let main files =
Coqide_ui.ui_m#insert_action_group windows_actions 0;
Coqide_ui.ui_m#insert_action_group help_actions 0;
w#add_accel_group Coqide_ui.ui_m#get_accel_group ;
+ GtkMain.Rc.parse_string "gtk-can-change-accels = 1";
if Coq_config.gtk_platform <> `QUARTZ
then vbox#pack (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar");
let tbar = GtkButton.Toolbar.cast ((Coqide_ui.ui_m#get_widget "/CoqIde ToolBar")#as_widget)
diff --git a/ide/coqide.mli b/ide/coqide.mli
index 57158a6a..18df1f6a 100644
--- a/ide/coqide.mli
+++ b/ide/coqide.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(*
#include
#include
-#include
+#include
GtkOSXApplication *theApp;
value open_file_fun, forbid_quit_fun, themenubar, pref_item, about_item;
@@ -76,10 +76,10 @@ CAMLprim value caml_gtk_mac_ready(value menubar, value prefs, value about)
caml_register_generational_global_root(&about_item);
/* gtk_accel_map_foreach(NULL, osx_accel_map_foreach_lcb);*/
gtk_osxapplication_set_menu_bar(theApp,check_cast(GTK_MENU_SHELL,themenubar));
- about_grp = gtk_osxapplication_add_app_menu_group(theApp);
- pref_grp = gtk_osxapplication_add_app_menu_group(theApp);
- gtk_osxapplication_add_app_menu_item(theApp,about_grp,check_cast(GTK_MENU_ITEM,about_item));
- gtk_osxapplication_add_app_menu_item(theApp,pref_grp,check_cast(GTK_MENU_ITEM,pref_item));
+ gtk_osxapplication_insert_app_menu_item(theApp,check_cast(GTK_WIDGET,about_item),1);
+ gtk_osxapplication_insert_app_menu_item(theApp,gtk_separator_menu_item_new(),2);
+ gtk_osxapplication_insert_app_menu_item(theApp,check_cast(GTK_WIDGET,pref_item),3);
+ gtk_osxapplication_insert_app_menu_item(theApp,gtk_separator_menu_item_new(),4);
gtk_osxapplication_ready(theApp);
CAMLreturn(Val_unit);
}
diff --git a/ide/ideproof.ml b/ide/ideproof.ml
index b79d6469..697e7f4f 100644
--- a/ide/ideproof.ml
+++ b/ide/ideproof.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* []
+| (lg, rg) :: l ->
+ let inner = flatten l in
+ List.rev_append lg inner @ rg
+
let display mode (view:GText.view) goals hints evars =
let () = view#buffer#set_text "" in
match goals with
| None -> ()
(* No proof in progress *)
- | Some { Interface.fg_goals = []; Interface.bg_goals = [] } ->
- (* A proof has been finished, but not concluded *)
- begin match evars with
- | Some evs when evs <> [] ->
+ | Some { Interface.fg_goals = []; Interface.bg_goals = bg } ->
+ let bg = flatten (List.rev bg) in
+ let evars = match evars with None -> [] | Some evs -> evs in
+ begin match (bg, evars) with
+ | [], [] ->
+ view#buffer#insert "No more subgoals."
+ | [], _ :: _ ->
+ (* A proof has been finished, but not concluded *)
view#buffer#insert "No more subgoals but non-instantiated existential variables:\n\n";
let iter evar =
let msg = Printf.sprintf "%s\n" evar.Interface.evar_info in
view#buffer#insert msg
in
- List.iter iter evs
- | _ ->
- view#buffer#insert "No more subgoals."
+ List.iter iter evars
+ | _, _ ->
+ (* No foreground proofs, but still unfocused ones *)
+ view#buffer#insert "This subproof is complete, but there are still unfocused goals:\n\n";
+ let iter goal =
+ let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in
+ view#buffer#insert msg
+ in
+ List.iter iter bg
end
- | Some { Interface.fg_goals = []; Interface.bg_goals = bg } ->
- (* No foreground proofs, but still unfocused ones *)
- view#buffer#insert "This subproof is complete, but there are still unfocused goals:\n\n";
- let iter goal =
- let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in
- view#buffer#insert msg
- in
- List.iter iter bg
| Some { Interface.fg_goals = fg } ->
mode view fg hints
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index a208ad0e..164c837a 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* /C_anonical Structure/" "")
-; (gtk_accel_path "/M_odule Type/" "")
-; (gtk_accel_path "/c_ompute/" "")
-; (gtk_accel_path "/Templates/_E.../" "")
-(gtk_accel_path "/Templates/match" "c")
-; (gtk_accel_path "/D_erive Inversion/" "")
-; (gtk_accel_path "/Queries/Check" "F3")
-; (gtk_accel_path "/i_dtac/" "")
-; (gtk_accel_path "/L_oad/" "")
-; (gtk_accel_path "/a_ssert/" "")
-; (gtk_accel_path "/f_irstorder using/" "")
-; (gtk_accel_path "/s_olve/" "")
-; (gtk_accel_path "/Tactics/_l.../" "")
-(gtk_accel_path "/Templates/Inductive" "i")
-; (gtk_accel_path "/a_ssert (__:__)/" "")
-; (gtk_accel_path "/T_est Printing Synth/" "")
-; (gtk_accel_path "/Templates/_R.../" "")
-; (gtk_accel_path "/Help/Browse Coq Library" "")
-; (gtk_accel_path "/U_nset Extraction Optimize/" "")
-; (gtk_accel_path "/s_imple inversion/" "")
-(gtk_accel_path "/Edit/Copy" "c")
-; (gtk_accel_path "/E_xtract Inductive/" "")
-(gtk_accel_path "/Edit/Cut" "x")
-; (gtk_accel_path "/i_nfo/" "")
-; (gtk_accel_path "/R_emove Printing If/" "")
-; (gtk_accel_path "/e_apply/" "")
-; (gtk_accel_path "/F_ixpoint/" "")
-; (gtk_accel_path "/c_hange __ in/" "")
-; (gtk_accel_path "/l_apply/" "")
-; (gtk_accel_path "/s_imple induction/" "")
-; (gtk_accel_path "/f_ail/" "")
-; (gtk_accel_path "/e_lim/" "")
-; (gtk_accel_path "/r_ewrite <- __ in/" "")
-; (gtk_accel_path "/A_dd Printing Let/" "")
-; (gtk_accel_path "/T_ransparent/" "")
-; (gtk_accel_path "/Tactics/_d.../" "")
-(gtk_accel_path "/Tactics/Wizard" "dollar")
+; (gtk_accel_path "/Templates/Template Read Module" "")
+; (gtk_accel_path "/Tactics/Tactic pattern" "")
+(gtk_accel_path "/Templates/Definition" "d")
+; (gtk_accel_path "/Templates/Template Program Lemma" "")
+(gtk_accel_path "/Templates/Lemma" "l")
+; (gtk_accel_path "/Templates/Template Fact" "")
+(gtk_accel_path "/Tactics/auto" "a")
+; (gtk_accel_path "/Tactics/Tactic fold" "")
+; (gtk_accel_path "/Help/About Coq" "")
+; (gtk_accel_path "/Templates/Template Add Ring A Aplus Amult Aone Azero Ainv Aeq T [ c1 ... cn ]. " "")
+; (gtk_accel_path "/Templates/Template Hypothesis" "")
+; (gtk_accel_path "/Tactics/Tactic repeat" "")
+; (gtk_accel_path "/Templates/Template Unset Extraction Optimize" "")
+; (gtk_accel_path "/Templates/Template Add Printing Constructor" "")
; (gtk_accel_path "/Windows/Detach View" "")
-; (gtk_accel_path "/T_heorem/" "")
-(gtk_accel_path "/Templates/Scheme" "s")
-; (gtk_accel_path "/R_emark/" "")
-; (gtk_accel_path "/Compile/Compile" "")
-; (gtk_accel_path "/A_dd Relation/" "")
-; (gtk_accel_path "/r_ename __ into/" "")
-; (gtk_accel_path "/File/Save as" "")
-; (gtk_accel_path "/f_irstorder/" "")
-; (gtk_accel_path "/G_rammar/" "")
-; (gtk_accel_path "/f_irstorder with/" "")
-; (gtk_accel_path "/r_ed/" "")
-; (gtk_accel_path "/D_efinition/" "")
-; (gtk_accel_path "/R_equire Import/" "")
-; (gtk_accel_path "/d_iscriminate/" "")
-; (gtk_accel_path "/i_ntro after/" "")
-; (gtk_accel_path "/Export/Latex" "")
-; (gtk_accel_path "/j_p/" "")
-; (gtk_accel_path "/a_uto with/" "")
-; (gtk_accel_path "/S_ection/" "")
-; (gtk_accel_path "/r_ewrite/" "")
-; (gtk_accel_path "/Export/Html" "")
-; (gtk_accel_path "/Tactics/_i.../" "")
-; (gtk_accel_path "/a_utorewrite/" "")
-; (gtk_accel_path "/F_ocus/" "")
-; (gtk_accel_path "/Templates/_O.../" "")
-; (gtk_accel_path "/l_azy in/" "")
-; (gtk_accel_path "/d_ependent inversion__clear __ with/" "")
-; (gtk_accel_path "/c_utrewrite/" "")
-(gtk_accel_path "/Edit/Undo" "u")
-; (gtk_accel_path "/c_onstructor __ with/" "")
-; (gtk_accel_path "/r_ing/" "")
-; (gtk_accel_path "/d_ependent rewrite <-/" "")
-; (gtk_accel_path "/e_limtype/" "")
-(gtk_accel_path "/Tactics/simpl" "s")
-; (gtk_accel_path "/H_int/" "")
-; (gtk_accel_path "/H_int Rewrite/" "")
-; (gtk_accel_path "/V_ariable/" "")
-; (gtk_accel_path "/U_nset Implicit Arguments/" "")
-; (gtk_accel_path "/s_implify__eq/" "")
-; (gtk_accel_path "/Compile/Next error" "F7")
-; (gtk_accel_path "/Edit/Edit" "")
-; (gtk_accel_path "/S_et Extraction Optimize/" "")
-; (gtk_accel_path "/H_ypothesis/" "")
-; (gtk_accel_path "/E_nd Silent./" "")
-; (gtk_accel_path "/S_yntax/" "")
-; (gtk_accel_path "/d_ecide equality/" "")
-; (gtk_accel_path "/O_paque/" "")
-; (gtk_accel_path "/Templates/_T.../" "")
-; (gtk_accel_path "/Tactics/_a.../" "")
-; (gtk_accel_path "/Templates/_G.../" "")
-; (gtk_accel_path "/c_ase/" "")
-(gtk_accel_path "/Navigation/Backward" "Up")
-; (gtk_accel_path "/C_oFixpoint/" "")
-; (gtk_accel_path "/P_rogram Fixpoint/" "")
-; (gtk_accel_path "/d_ependent inversion__clear/" "")
-; (gtk_accel_path "/c_ase __ with/" "")
-; (gtk_accel_path "/a_ssumption/" "")
-; (gtk_accel_path "/t_ransitivity/" "")
-; (gtk_accel_path "/i_ntros until/" "")
-; (gtk_accel_path "/s_plit/" "")
-; (gtk_accel_path "/e_xists/" "")
-(gtk_accel_path "/Templates/Theorem" "t")
-; (gtk_accel_path "/Navigation/Navigation" "")
-; (gtk_accel_path "/H_int Unfold/" "")
-; (gtk_accel_path "/I_mplicit Arguments/" "")
-; (gtk_accel_path "/Help/Help" "")
-; (gtk_accel_path "/d_ecompose sum/" "")
-; (gtk_accel_path "/A_dd Abstract Ring A Aplus Amult Aone Azero Ainv Aeq T./" "")
-; (gtk_accel_path "/Te_mplates/" "")
-(gtk_accel_path "/Edit/Find in buffer" "f")
-; (gtk_accel_path "/r_eplace __ with/" "")
-(gtk_accel_path "/Tactics/omega" "o")
-; (gtk_accel_path "/S_cheme/" "")
-; (gtk_accel_path "/L_emma/" "")
-; (gtk_accel_path "/i_nversion__clear __ in/" "")
-; (gtk_accel_path "/E_xtraction Inline/" "")
-; (gtk_accel_path "/S_yntactic Definition/" "")
-; (gtk_accel_path "/i_nstantiate (__:=__)/" "")
-; (gtk_accel_path "/C_hapter/" "")
-; (gtk_accel_path "/Templates/_L.../" "")
-; (gtk_accel_path "/Tactics/_f.../" "")
-; (gtk_accel_path "/Queries/Queries" "")
-; (gtk_accel_path "/T_est Printing Wildcard/" "")
-(gtk_accel_path "/File/Open" "o")
-; (gtk_accel_path "/f_old __ in/" "")
-(gtk_accel_path "/Navigation/Go to" "Right")
+; (gtk_accel_path "/Tactics/Tactic inversion" "")
+; (gtk_accel_path "/Templates/Template Write State" "")
; (gtk_accel_path "/Export/Export to" "")
-; (gtk_accel_path "/c_ongruence/" "")
-; (gtk_accel_path "/c_learbody/" "")
-(gtk_accel_path "/File/Close buffer" "w")
-; (gtk_accel_path "/a_pply/" "")
-; (gtk_accel_path "/Queries/SearchAbout" "F2")
-; (gtk_accel_path "/i_ntro/" "")
-; (gtk_accel_path "/H_int Immediate/" "")
-; (gtk_accel_path "/p_ose __:=__)/" "")
-; (gtk_accel_path "/U_nset Undo/" "")
-; (gtk_accel_path "/Tactics/_s.../" "")
-; (gtk_accel_path "/P_rogram Definition/" "")
-; (gtk_accel_path "/R_equire/" "")
-; (gtk_accel_path "/c_ompare/" "")
-; (gtk_accel_path "/s_ymmetry in/" "")
-(gtk_accel_path "/Display/Display coercions" "c")
-(gtk_accel_path "/Navigation/Previous" "less")
-(gtk_accel_path "/Display/Display all low-level contents" "l")
-; (gtk_accel_path "/C_oercion Local/" "")
-; (gtk_accel_path "/f_ix __ with/" "")
-; (gtk_accel_path "/A_dd ML Path/" "")
-; (gtk_accel_path "/A_xiom/" "")
-; (gtk_accel_path "/Templates/Templates" "")
-; (gtk_accel_path "/a_bstract/" "")
-; (gtk_accel_path "/Edit/Clear Undo Stack" "")
-(gtk_accel_path "/File/New" "n")
-; (gtk_accel_path "/Tactics/_hnf/" "")
-; (gtk_accel_path "/d_o/" "")
-; (gtk_accel_path "/E_xtract Constant/" "")
-; (gtk_accel_path "/E_nd/" "")
-; (gtk_accel_path "/Templates/_Qed./" "")
-; (gtk_accel_path "/A_dd Rec ML Path/" "")
-; (gtk_accel_path "/Templates/_D.../" "")
-(gtk_accel_path "/Navigation/Hide" "h")
-; (gtk_accel_path "/c_ofix/" "")
-; (gtk_accel_path "/_Try Tactics/" "")
-; (gtk_accel_path "/S_et Printing Wildcard/" "")
-; (gtk_accel_path "/i_nversion__clear/" "")
-; (gtk_accel_path "/Templates/_V.../" "")
+(gtk_accel_path "/Tactics/auto with *" "asterisk")
+; (gtk_accel_path "/Tactics/Tactic inversion--clear" "")
+; (gtk_accel_path "/Templates/Template Implicit Arguments" "")
+(gtk_accel_path "/Edit/Find backwards" "b")
+; (gtk_accel_path "/Edit/Copy" "c")
+; (gtk_accel_path "/Tactics/Tactic inversion -- using" "")
+(gtk_accel_path "/View/Previous tab" "Left")
+; (gtk_accel_path "/Tactics/Tactic change -- in" "")
+; (gtk_accel_path "/Tactics/Tactic jp" "")
+; (gtk_accel_path "/Tactics/Tactic red" "")
+; (gtk_accel_path "/Templates/Template Coercion" "")
+; (gtk_accel_path "/Templates/Template CoFixpoint" "")
+; (gtk_accel_path "/Tactics/Tactic intros until" "")
+; (gtk_accel_path "/Templates/Template Derive Dependent Inversion" "")
+; (gtk_accel_path "/Tactics/Tactic eapply" "")
+; (gtk_accel_path "/View/View" "")
+; (gtk_accel_path "/Tactics/Tactic change" "")
+; (gtk_accel_path "/Tactics/Tactic firstorder using" "")
+; (gtk_accel_path "/Tactics/Tactic decompose sum" "")
+; (gtk_accel_path "/Tactics/Tactic cut" "")
+; (gtk_accel_path "/Templates/Template Remove Printing Let" "")
+; (gtk_accel_path "/Templates/Template Structure" "")
+; (gtk_accel_path "/Tactics/Tactic compute in" "")
+; (gtk_accel_path "/Queries/Locate" "")
+; (gtk_accel_path "/Templates/Template Save." "")
+; (gtk_accel_path "/Templates/Template Canonical Structure" "")
+; (gtk_accel_path "/Tactics/Tactic compare" "")
+; (gtk_accel_path "/Templates/Template Next Obligation" "")
+(gtk_accel_path "/View/Display notations" "n")
+; (gtk_accel_path "/Tactics/Tactic fail" "")
+; (gtk_accel_path "/Tactics/Tactic left" "")
+(gtk_accel_path "/Edit/Undo" "u")
+(gtk_accel_path "/Tactics/eauto with *" "