- Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used to

  change the default pretty-printing to use Π, λ instead of
  forall and fun (and allow "," as well as "=>" for "fun" to be more
  consistent with the standard forall and exists syntax). Parsing allows
  theses new forms too, even if not in -unicode, and does not make Π or
  λ keywords. As usual, criticism and suggestions are welcome :)
  Not sure what to do about "->"/"→" ?
- [setoid_replace by] now uses tactic3() to get the right parsing level
  for tactics. 
- Type class [Instance] names are now mandatory.
- Document [rewrite at/by] and fix parsing of occs to support their
  combination.
- Backtrack on [Enriching] modifier, now used exclusively in the 
  implementation of implicit arguments.


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

2 files changed, 13 insertions, 14 deletions

diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index aeaa197e8..aea6f5d7a 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -76,23 +76,23 @@ Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   setoidreplaceinat (default_relation x y) id idtac o.
 
 Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
-  "by" tactic(t) :=
+  "by" tactic3(t) :=
   setoidreplace (default_relation x y) ltac:t.
 
 Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
   "at" int_or_var_list(o) 
-  "by" tactic(t) :=
+  "by" tactic3(t) :=
   setoidreplaceat (default_relation x y) ltac:t o.
 
 Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
   "in" hyp(id) 
-  "by" tactic(t) :=
+  "by" tactic3(t) :=
   setoidreplacein (default_relation x y) id ltac:t.
 
 Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
   "in" hyp(id) 
   "at" int_or_var_list(o) 
-  "by" tactic(t) :=
+  "by" tactic3(t) :=
   setoidreplaceinat (default_relation x y) id ltac:t o.
 
 Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
@@ -106,13 +106,13 @@ Tactic Notation "setoid_replace" constr(x) "with" constr(y)
 
 Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
   "using" "relation" constr(rel) 
-  "by" tactic(t) :=
+  "by" tactic3(t) :=
   setoidreplace (rel x y) ltac:t.
 
 Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
   "using" "relation" constr(rel) 
   "at" int_or_var_list(o)  
-  "by" tactic(t) :=
+  "by" tactic3(t) :=
   setoidreplaceat (rel x y) ltac:t o.
 
 Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
@@ -129,14 +129,14 @@ Tactic Notation "setoid_replace" constr(x) "with" constr(y)
 Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
   "using" "relation" constr(rel)
   "in" hyp(id)
-  "by" tactic(t) :=
+  "by" tactic3(t) :=
   setoidreplacein (rel x y) id ltac:t.
 
 Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
   "using" "relation" constr(rel) 
   "in" hyp(id)
   "at" int_or_var_list(o)  
-  "by" tactic(t) :=
+  "by" tactic3(t) :=
   setoidreplaceinat (rel x y) id ltac:t o.
 
 (** The [add_morphism_tactic] tactic is run at each [Add Morphism] command before giving the hand back
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index d24312ff1..cbc3b02ad 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -4,7 +4,7 @@ Require Import ProofIrrelevance.
 
 Open Local Scope program_scope.
 
-Implicit Arguments Enriching Acc_inv [y].
+Implicit Arguments Acc_inv [A R x y].
 
 (** Reformulation of the Wellfounded module using subsets where possible. *)
 
@@ -137,11 +137,10 @@ Section Well_founded_measure.
       apply Fix_measure_F_inv.
     Qed.
 
-    Lemma fix_measure_sub_eq :
-        forall x : A,
-          Fix_measure_sub P F_sub x =
-          let f_sub := F_sub in
-            f_sub x (fun (y : A | m y < m x) => Fix_measure (`y)).
+    Lemma fix_measure_sub_eq : forall x : A,
+      Fix_measure_sub P F_sub x =
+        let f_sub := F_sub in
+          f_sub x (fun (y : A | m y < m x) => Fix_measure (`y)).
       exact Fix_measure_eq.
     Qed.