From 7248f6cccfcca2b0d59b244e8789590794aefc45 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Mon, 12 May 2008 12:27:25 +0000
Subject: - 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
---
 theories/Program/Wf.v | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

(limited to 'theories/Program')

diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index d24312ff13..cbc3b02ad9 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.
 
-- 
cgit v1.2.3