A little bit of cleanup, and some annotations.

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

1 files changed, 10 insertions, 8 deletions

diff --git a/plugins/micromega/VarMap.v b/plugins/micromega/VarMap.v
index 0a66fce35..c0bf05634 100644
--- a/plugins/micromega/VarMap.v
+++ b/plugins/micromega/VarMap.v
@@ -18,11 +18,12 @@ Require Import Coq.Arith.Max.
 Require Import List.
 Set Implicit Arguments.
 
-(* I have addded a Leaf constructor to the varmap data structure (/plugins/ring/Quote.v)
-   -- this is harmless and spares a lot of Empty.
-   This means smaller proof-terms.
-   BTW, by dropping the  polymorphism, I get small (yet noticeable) speed-up.
-*)
+(* 
+ * This adds a Leaf constructor to the varmap data structure (plugins/quote/Quote.v)
+ * --- it is harmless and spares a lot of Empty.
+ * It also means smaller proof-terms.
+ * As a side note, by dropping the polymorphism, one gets small, yet noticeable, speed-up.
+ *)
 
 Section MakeVarMap.
   Variable A : Type.
@@ -33,7 +34,7 @@ Section MakeVarMap.
   | Leaf : A -> t
   | Node : t  -> A -> t  -> t .
 
-  Fixpoint find   (vm : t ) (p:positive) {struct vm} : A :=
+  Fixpoint find (vm : t) (p:positive) {struct vm} : A :=
     match vm with
       | Empty => default
       | Leaf i => i
@@ -44,8 +45,9 @@ Section MakeVarMap.
                       end
     end.
 
- (* an off_map (a map with offset) offers the same functionalites  as /plugins/setoid_ring/BinList.v - it is used in EnvRing.v *)
-(*
+  (* FK: scheduled for deletion *)
+  (* an off_map (a map with offset) offers the same functionalites  as /plugins/setoid_ring/BinList.v - it is used in EnvRing.v *)
+  (*
   Definition off_map  :=  (option positive *t )%type.