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