This fixes (-2) mod 2 being evaluated as nonzero.

Martin Clochard authored Jul 20, 2015 and Guillaume Melquiond committed Oct 13, 2015

ECase(ghost e1,[branch]) and constructor application with ghost parameters
were handled incorrectly.

Martin Clochard authored Sep 17, 2015 and Guillaume Melquiond committed Oct 13, 2015

The following could be proved correct:

type t = A | B
function f (x:'a) : 'a = x
predicate top = A = f A
lemma bad : forall x:t. match x with A -> x = B | B -> x = B -> top end
lemma fail : false

The first one is the main file, the rest only supply
rules for individual theories and modules.

in anticipation of future module refinement

features polymorphic recursion, both in the logic and in programs