diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-04-07 15:50:26 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-04-07 20:12:09 +0200 |
| commit | 9f0a896536e709880de5ba638069dea680803f62 (patch) | |
| tree | 5cb3cbc5e54ed4e1037e854949a38a387a20c0b1 /test-suite/bugs/closed | |
| parent | 83608720aac2a0a464649aca8b2a23ce395679ae (diff) | |
Allow to unset the refinement mode of Instance in ML
Falling back to the global setting if not given.
Useful to make Add Morphism fail correctly when the given proof terms
are incomplete. Adapt test-suite file #2848 accordingly.
Diffstat (limited to 'test-suite/bugs/closed')
| -rw-r--r-- | test-suite/bugs/closed/2848.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/test-suite/bugs/closed/2848.v b/test-suite/bugs/closed/2848.v index de137d39d..828e3b8c1 100644 --- a/test-suite/bugs/closed/2848.v +++ b/test-suite/bugs/closed/2848.v @@ -2,8 +2,9 @@ Require Import Setoid. Parameter value' : Type. Parameter equiv' : value' -> value' -> Prop. - +Axiom cheat : forall {A}, A. Add Parametric Relation : _ equiv' - reflexivity proved by (Equivalence.equiv_reflexive _) - transitivity proved by (Equivalence.equiv_transitive _) + reflexivity proved by (Equivalence.equiv_reflexive cheat) + transitivity proved by (Equivalence.equiv_transitive cheat) as apply_equiv'_rel. +Check apply_equiv'_rel : PreOrder equiv'.
\ No newline at end of file |