From 6e847be2a6846ab11996d2774b6bc507a342a626 Mon Sep 17 00:00:00 2001
From: Frédéric Besson
Date: Wed, 7 Sep 2016 10:28:07 +0200
Subject: micromega : more robust generation of proof terms

- Assert a purely arihtmetic sub-goal that is proved independently by reflexion.
  (This reduces the stress on the conversion test)
- Does not use 'abstract' anymore (more natural proof-term)
- Fix a parsing bug (certain terms in Prop where not recognized)
---
 plugins/micromega/VarMap.v | 29 +++++++++++++++++++++++++++--
 1 file changed, 27 insertions(+), 2 deletions(-)

(limited to 'plugins/micromega/VarMap.v')

diff --git a/plugins/micromega/VarMap.v b/plugins/micromega/VarMap.v
index 4981ddb302..2d2c0bc77a 100644
--- a/plugins/micromega/VarMap.v
+++ b/plugins/micromega/VarMap.v
@@ -1,7 +1,7 @@
 (* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -26,6 +26,7 @@ Set Implicit Arguments.
  *)
 
 Section MakeVarMap.
+  
   Variable A : Type.
   Variable default : A.
 
@@ -46,5 +47,29 @@ Section MakeVarMap.
     end.
 
 
-End MakeVarMap.
+  Fixpoint singleton (x:positive) (v : A) : t :=
+    match x with
+    | xH => Leaf v
+    | xO p => Node (singleton p v) default Empty
+    | xI p => Node Empty default (singleton p v)
+    end.
+  
+  Fixpoint vm_add (x: positive) (v : A) (m : t) {struct m} : t :=
+    match m with
+    | Empty   => singleton x v
+    | Leaf vl =>
+      match x with
+      | xH => Leaf v
+      | xO p => Node (singleton p v) vl Empty
+      | xI p => Node Empty vl (singleton p v)
+      end
+    | Node l o r => 
+      match x with
+      | xH => Node l v r
+      | xI p => Node l o (vm_add p v r)
+      | xO p => Node (vm_add p v l) o r
+      end
+    end.
 
+  
+End MakeVarMap.  
-- 
cgit v1.2.3