diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-05-17 15:22:49 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-05-22 15:26:59 +0200 |
| commit | d992ae9fc539bdadd9214d2c92d83bd08b68ef33 (patch) | |
| tree | 428064afb1b0cac346a05fc4bb61f3573abe8505 /plugins/romega/const_omega.ml | |
| parent | a1b6cb8c2742bc76707db8d13abbbd2d218b6486 (diff) | |
ROmega : O_STATE turned into a O_SUM
We benefit from the fact that we normalize now *all* hypotheses
even the one defining the "stated" variable: it is produced as
...def of v... = v
and normalized as
-v + ...def of v... = 0
which is precisely what we should add to the initial equation during
a O_STATE.
Diffstat (limited to 'plugins/romega/const_omega.ml')
| -rw-r--r-- | plugins/romega/const_omega.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index 6e2fa5ed3..ce47ef16a 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -106,7 +106,6 @@ 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") let coq_s_sum = lazy (constant "O_SUM") -let coq_s_state = lazy (constant "O_STATE") let coq_s_merge_eq = lazy (constant "O_MERGE_EQ") let coq_s_split_ineq =lazy (constant "O_SPLIT_INEQ") |