- 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

1 files changed, 5 insertions, 6 deletions

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.