diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-05-17 13:39:59 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-05-22 15:26:59 +0200 |
| commit | 7509f5c8eab84fda5a9029329c6b70758259765f (patch) | |
| tree | 64b2d9b007f2a09ea3e2d1dcec8a774d54437427 /plugins/romega/const_omega.ml | |
| parent | eae11e85b5fe578fbec404b91628062aa255be92 (diff) | |
ROmega : merge O_CONSTANT* into a single O_BAD_CONSTANT
Diffstat (limited to 'plugins/romega/const_omega.ml')
| -rw-r--r-- | plugins/romega/const_omega.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index 4fd224e2b..fa92903ba 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -101,8 +101,7 @@ let coq_p_and = lazy (constant "Tand") let coq_p_imp = lazy (constant "Timp") let coq_p_prop = lazy (constant "Tprop") -let coq_s_constant_not_nul = lazy (constant "O_CONSTANT_NOT_NUL") -let coq_s_constant_neg = lazy (constant "O_CONSTANT_NEG") +let coq_s_bad_constant = lazy (constant "O_BAD_CONSTANT") let coq_s_div_approx = lazy (constant "O_DIV_APPROX") let coq_s_not_exact_divide = lazy (constant "O_NOT_EXACT_DIVIDE") let coq_s_exact_divide = lazy (constant "O_EXACT_DIVIDE") @@ -111,7 +110,6 @@ let coq_s_state = lazy (constant "O_STATE") let coq_s_contradiction = lazy (constant "O_CONTRADICTION") let coq_s_merge_eq = lazy (constant "O_MERGE_EQ") let coq_s_split_ineq =lazy (constant "O_SPLIT_INEQ") -let coq_s_constant_nul =lazy (constant "O_CONSTANT_NUL") let coq_s_negate_contradict =lazy (constant "O_NEGATE_CONTRADICT") let coq_s_negate_contradict_inv =lazy (constant "O_NEGATE_CONTRADICT_INV") |