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 /tools/gallina-syntax.el | |
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 'tools/gallina-syntax.el')
0 files changed, 0 insertions, 0 deletions