diff options
Diffstat (limited to 'plugins/romega/const_omega.ml')
| -rw-r--r-- | plugins/romega/const_omega.ml | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index fa92903ba..6e2fa5ed3 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -107,11 +107,8 @@ let coq_s_not_exact_divide = lazy (constant "O_NOT_EXACT_DIVIDE") let coq_s_exact_divide = lazy (constant "O_EXACT_DIVIDE") let coq_s_sum = lazy (constant "O_SUM") 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_negate_contradict =lazy (constant "O_NEGATE_CONTRADICT") -let coq_s_negate_contradict_inv =lazy (constant "O_NEGATE_CONTRADICT_INV") (* construction for the [extract_hyp] tactic *) let coq_direction = lazy (constant "direction") |