From 4fc5ff31b342253f889db23a3b46482a4c7fa1ca Mon Sep 17 00:00:00 2001 From: fkirchne Date: Fri, 28 May 2010 16:40:21 +0000 Subject: 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 --- plugins/micromega/VarMap.v | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) (limited to 'plugins/micromega/VarMap.v') 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. -- cgit v1.2.3