diff options
| author | herbelin | 2008-05-20 15:51:40 +0000 |
|---|---|---|
| committer | herbelin | 2008-05-20 15:51:40 +0000 |
| commit | cfbe8d0bca1cb0d84e3d7bfbae19fb1446e4ca17 (patch) | |
| tree | 6733627e49bbb10f0d82885f60930fd988c532cc /contrib | |
| parent | 4aa8d2cdea256368ffb968c933308a4420774239 (diff) | |
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
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/micromega/coq_micromega.ml | 1 |
1 files changed, 1 insertions, 0 deletions
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 |