Final part of moving Program code inside the main code. Adapted add_definition/fixpoint and parsing of the "Program" prefix.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15036 85f007b7-540e-0410-9357-904b9bb8a0f7

8 files changed, 21 insertions, 20 deletions

diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
index 9c600b01e..9f44d4fef 100644
--- a/theories/Classes/EquivDec.v
+++ b/theories/Classes/EquivDec.v
@@ -141,5 +141,5 @@ Program Instance list_eqdec `(eqa : EqDec A eq) : ! EqDec (list A) eq :=
 
   Next Obligation. destruct y ; intuition eauto. Defined.
 
-  Solve Obligations using unfold equiv, complement in * ; 
+  Solve Obligations with unfold equiv, complement in * ; 
     program_simpl ; intuition (discriminate || eauto).
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index d9e9fe257..afdfb4cec 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -105,13 +105,15 @@ Section Respecting.
   (** Here we build an equivalence instance for functions which relates respectful ones only,
      we do not export it. *)
 
-  Definition respecting `(eqa : Equivalence A (R : relation A), eqb : Equivalence B (R' : relation B)) : Type :=
+  Definition respecting `(eqa : Equivalence A (R : relation A), 
+                          eqb : Equivalence B (R' : relation B)) : Type :=
     { morph : A -> B | respectful R R' morph morph }.
 
   Program Instance respecting_equiv `(eqa : Equivalence A R, eqb : Equivalence B R') :
-    Equivalence (fun (f g : respecting eqa eqb) => forall (x y : A), R x y -> R' (proj1_sig f x) (proj1_sig g y)).
+    Equivalence (fun (f g : respecting eqa eqb) => 
+                   forall (x y : A), R x y -> R' (proj1_sig f x) (proj1_sig g y)).
 
-  Solve Obligations using unfold respecting in * ; simpl_relation ; program_simpl.
+  Solve Obligations with unfold respecting in * ; simpl_relation ; program_simpl.
 
   Next Obligation.
   Proof.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 8e491b1b8..e0d7a3d7a 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -224,7 +224,7 @@ Hint Extern 4 (subrelation (inverse _) _) =>
   class_apply @subrelation_symmetric : typeclass_instances.
 
 (** The complement of a relation conserves its proper elements. *)
-
+Set Printing All.
 Program Definition complement_proper
   `(mR : Proper (A -> A -> Prop) (RA ==> RA ==> iff) R) :
   Proper (RA ==> RA ==> iff) (complement R) := _.
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index 6708220ea..a090d2007 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -108,7 +108,7 @@ Program Instance prod_eqdec `(! EqDec (eq_setoid A), ! EqDec (eq_setoid B))
       else in_right
     else in_right.
 
-  Solve Obligations using unfold complement ; program_simpl.
+  Solve Obligations with unfold complement ; program_simpl.
 
 (** Objects of function spaces with countable domains like bool
   have decidable equality. *)
@@ -121,7 +121,7 @@ Program Instance bool_function_eqdec `(! EqDec (eq_setoid A))
       else in_right
     else in_right.
 
-  Solve Obligations using try red ; unfold equiv, complement ; program_simpl.
+  Solve Obligations with try red ; unfold equiv, complement ; program_simpl.
 
   Next Obligation.
   Proof.
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index 2e2eb166d..6d0315b82 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -494,9 +494,9 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
 
   Definition lt_key (p p':positive*A) := E.lt (fst p) (fst p').
 
-  Global Program Instance eqk_equiv : Equivalence eq_key.
-  Global Program Instance eqke_equiv : Equivalence eq_key_elt.
-  Global Program Instance ltk_strorder : StrictOrder lt_key.
+  Global Instance eqk_equiv : Equivalence eq_key := _.
+  Global Instance eqke_equiv : Equivalence eq_key_elt := _.
+  Global Instance ltk_strorder : StrictOrder lt_key := _.
 
   Lemma mem_find :
     forall m x, mem x m = match find x m with None => false | _ => true end.
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index e929c561c..4b3c1b4fb 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -21,7 +21,6 @@ Declare ML Module "cc_plugin".
 Declare ML Module "ground_plugin".
 Declare ML Module "dp_plugin".
 Declare ML Module "recdef_plugin".
-Declare ML Module "subtac_plugin".
 Declare ML Module "xml_plugin".
 (* Default substrings not considered by queries like SearchAbout *)
 Add Search Blacklist "_admitted" "_subproof" "Private_".
diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v
index ca4002d7f..dda0ed68d 100644
--- a/theories/Program/Subset.v
+++ b/theories/Program/Subset.v
@@ -79,14 +79,14 @@ Qed.
 (* Somewhat trivial definition, but not unfolded automatically hence we can match on [match_eq ?A ?B ?x ?f]
    in tactics. *)
 
-Definition match_eq (A B : Type) (x : A) (fn : forall (y : A | y = x), B) : B :=
+Definition match_eq (A B : Type) (x : A) (fn : {y : A | y = x} -> B) : B :=
   fn (exist _ x eq_refl).
 
 (* This is what we want to be able to do: replace the originaly matched object by a new,
    propositionally equal one. If [fn] works on [x] it should work on any [y | y = x]. *)
 
-Lemma match_eq_rewrite : forall (A B : Type) (x : A) (fn : forall (y : A | y = x), B)
-  (y : A | y = x),
+Lemma match_eq_rewrite : forall (A B : Type) (x : A) (fn : {y : A | y = x} -> B)
+  (y : {y:A | y = x}),
   match_eq A B x fn = fn y.
 Proof.
   intros.
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index a823aedd3..ee0a7451b 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -35,11 +35,11 @@ Section Well_founded.
   Hypothesis
     F_ext :
     forall (x:A) (f g:forall y:{y:A | R y x}, P (`y)),
-      (forall (y : A | R y x), f y = g y) -> F_sub x f = F_sub x g.
+      (forall y:{y : A | R y x}, f y = g y) -> F_sub x f = F_sub x g.
 
   Lemma Fix_F_eq :
     forall (x:A) (r:Acc R x),
-      F_sub x (fun (y:A|R y x) => Fix_F_sub (`y) (Acc_inv r (proj2_sig y))) = Fix_F_sub x r.
+      F_sub x (fun y:{y:A | R y x} => Fix_F_sub (`y) (Acc_inv r (proj2_sig y))) = Fix_F_sub x r.
   Proof.
     destruct r using Acc_inv_dep; auto.
   Qed.
@@ -50,7 +50,7 @@ Section Well_founded.
     rewrite (proof_irrelevance (Acc R x) r s) ; auto.
   Qed.
 
-  Lemma Fix_eq : forall x:A, Fix_sub x = F_sub x (fun (y:A|R y x) => Fix_sub (proj1_sig y)).
+  Lemma Fix_eq : forall x:A, Fix_sub x = F_sub x (fun y:{ y:A | R y x} => Fix_sub (proj1_sig y)).
   Proof.
     intro x; unfold Fix_sub in |- *.
     rewrite <- (Fix_F_eq ).
@@ -62,7 +62,7 @@ Section Well_founded.
     forall x : A,
       Fix_sub x =
       let f_sub := F_sub in
-        f_sub x (fun (y : A | R y x) => Fix_sub (`y)).
+        f_sub x (fun y: {y : A | R y x} => Fix_sub (`y)).
     exact Fix_eq.
   Qed.
 
@@ -231,10 +231,10 @@ Module WfExtensionality.
   Program Lemma fix_sub_eq_ext :
     forall (A : Type) (R : A -> A -> Prop) (Rwf : well_founded R)
       (P : A -> Type)
-      (F_sub : forall x : A, (forall (y : A | R y x), P y) -> P x),
+      (F_sub : forall x : A, (forall y:{y : A | R y x}, P y) -> P x),
       forall x : A,
         Fix_sub A R Rwf P F_sub x =
-          F_sub x (fun (y : A | R y x) => Fix_sub A R Rwf P F_sub y).
+          F_sub x (fun y:{y : A | R y x} => Fix_sub A R Rwf P F_sub y).
   Proof.
     intros ; apply Fix_eq ; auto.
     intros.