diff options
| author |  fbesson <fbesson@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-05-23 18:00:22 +0000 |
|---|---|---|
| committer | fbesson <fbesson@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-05-23 18:00:22 +0000 |
| commit | a87b941bcdd0f3de75e18a245cbad4656fa11fe8 (patch) | |
| tree | f8aa894c6013ebdc56c394701370c8e208cf0df8 /plugins/micromega/coq_micromega.ml | |
| parent | f1686dbcad2515eee22b26b156fe51f6e9d22857 (diff) | |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14152 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/micromega/coq_micromega.ml')
| -rw-r--r-- | plugins/micromega/coq_micromega.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 69ec518ee..42d451a2d 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1524,6 +1524,7 @@ let rec abstract_wrt_formula f1 f2 = | I(a,_,b) , I(a',x,b') -> I(abstract_wrt_formula a a',x, abstract_wrt_formula b b') | FF , FF -> FF | TT , TT -> TT + | N x , N y -> N(abstract_wrt_formula x y) | _ -> failwith "abstract_wrt_formula" (** |