From cfbe8d0bca1cb0d84e3d7bfbae19fb1446e4ca17 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 20 May 2008 15:51:40 +0000
Subject: Corrections d'erreurs rapportées par Frédéric Besson sur le précédent
 commit de micromega + cache csdp complet.

Quelques questions résiduelles :
- où mettre l'interface entre coq et csdp (csdpcert) ?
- micromega.ml est un fichier engendré par extraction : vaut-il le
  coup de compiler coq en deux fois, une 1e fois pour compiler et
  extraire micromega.ml, une seconde fois pour inclure micromega.ml ?



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10955 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/micromega/coq_micromega.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'contrib')

diff --git a/contrib/micromega/coq_micromega.ml b/contrib/micromega/coq_micromega.ml
index 9fcc69173b..29e2a183af 100644
--- a/contrib/micromega/coq_micromega.ml
+++ b/contrib/micromega/coq_micromega.ml
@@ -803,6 +803,7 @@ let parse_rexpr =
 	let g,env = xparse_formula env b in
         mkformula_binary mkI term f g,env
     | _ when term = Lazy.force coq_True -> (TT,env)
+    | _ when term = Lazy.force coq_False -> (FF,env)
     | _  -> X(term),env in
   xparse_formula env term
 
-- 
cgit v1.2.3