new csdp cache + improved error message

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

1 files changed, 19 insertions, 0 deletions

diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v
index 65ea366fd..212478720 100644
--- a/plugins/micromega/ZMicromega.v
+++ b/plugins/micromega/ZMicromega.v
@@ -1081,6 +1081,25 @@ Proof.
   apply ZChecker_sound.
 Qed.
 
+Fixpoint xhyps_of_pt (base:nat) (acc : list nat) (pt:ZArithProof)  : list nat :=
+  match pt with
+    | DoneProof => acc
+    | RatProof c pt => xhyps_of_pt (S base ) (xhyps_of_psatz base acc c) pt
+    | CutProof c pt => xhyps_of_pt (S base ) (xhyps_of_psatz base acc c) pt
+    | EnumProof c1 c2 l => 
+      let acc := xhyps_of_psatz base (xhyps_of_psatz base acc c2) c1 in
+        List.fold_left (xhyps_of_pt (S base)) l acc
+  end.
+
+Definition hyps_of_pt (pt : ZArithProof) : list nat := xhyps_of_pt 0 nil pt.
+
+
+(*Lemma hyps_of_pt_correct : forall pt l, *)
+
+
+
+
+
 
 Open Scope Z_scope.