diff options
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 |