diff options
author | Jason Gross <jgross@mit.edu> | 2016-11-10 21:18:16 -0500 |
---|---|---|
committer | Jason Gross <jasongross9@gmail.com> | 2016-11-11 16:07:28 -0500 |
commit | 8e9b64460ac03810255529b16be49a8a4912d0d5 (patch) | |
tree | 071a84174e850e847e473646213f8fa2acade36c /src/Specific/GF25519Reflective | |
parent | 790e9ccfc164241e32d6fe4ba80c85e17cbb7051 (diff) |
8.4-compatible universe handling
Diffstat (limited to 'src/Specific/GF25519Reflective')
-rw-r--r-- | src/Specific/GF25519Reflective/Common.v | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/src/Specific/GF25519Reflective/Common.v b/src/Specific/GF25519Reflective/Common.v index c302926d6..8b500b42b 100644 --- a/src/Specific/GF25519Reflective/Common.v +++ b/src/Specific/GF25519Reflective/Common.v @@ -395,11 +395,13 @@ Notation compute_bounds opW bounds Module Export PrettyPrinting. - Section bounds_not_set. - Let T := let T := Type in let enforce := Set : T in T. - Inductive bounds_on : T := overflow | in_range (lower upper : Z). - End bounds_not_set. - Inductive result := yes | no. + (* We add [enlargen] to force [bounds_on] to be in [Type] in 8.4 and + 8.5/8.6. Because [Set] is special and things break if + [bounds_on] ends up in [Set] for reasons jgross hasn't bothered + to debug. *) + Inductive bounds_on := overflow | in_range (lower upper : Z) | enlargen (_ : Set). + + Inductive result := yes | no | borked. Definition ZBounds_to_bounds_on := fun t : base_type @@ -417,10 +419,12 @@ Module Export PrettyPrinting. | Tbase TZ => fun v => match v with | overflow => yes | in_range _ _ => no + | enlargen _ => borked end | Prod x y => fun v => match @does_it_overflow _ (fst v), @does_it_overflow _ (snd v) with | no, no => no - | _, _ => yes + | yes, no | no, yes | yes, yes => yes + | borked, _ | _, borked => borked end end. |