Omega: avoiding distinct proof-terms on repeated identical runs

 Omega now reuse the same inner variable names (Zvar0, Zvar1, ...)
 at each run. This way, the obtained proof-terms on
 two identical omega runs should be the same.
 This wasn't always the case earlier:
  - the two proofs were almost always convertible, but with distinct
    variable names.
  - in very rare situations, the two proofs could even be non-convertible.
    Indeed, the omega engine use hash-tables which may be sensible to
    the names in the (in)equality system and hence lead to different
    solutions. Example of this behavior (with ocaml 4, whose default hash
    function is different from ocaml 3.12, leading to a different behavior
    here !) :

--------------------------------------------------------------------
Require Import Omega.
Lemma test1 : forall i j, i < j -> i-1 < j. intros; omega. Defined.
Lemma test2 : forall i j, i < j -> i-1 < j. intros; omega. Defined.
Lemma test3 : forall i j, i < j -> i-1 < j. intros; omega. Defined.
Lemma test4 : forall i j, i < j -> i-1 < j. intros; omega. Defined.
Check (eq_refl : test1 = test2). (* OK *)
Check (eq_refl : test1 = test3). (* OK *)
Check (eq_refl : test1 = test4). (* KO, test4 is different !! *)
--------------------------------------------------------------------

 The old behavior could be restored with "Unset Stable Omega".

 Thanks to Frédéric Loulergue for spotting this sensibility to
 the underlying ocaml versions...

0 files changed, 0 insertions, 0 deletions