diff options
| -rw-r--r-- | tactics/rewrite.ml | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/2848.v | 7 | ||||
| -rw-r--r-- | toplevel/classes.ml | 4 | ||||
| -rw-r--r-- | toplevel/classes.mli | 1 |
4 files changed, 8 insertions, 6 deletions
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 21abafbf18..9d70c177b4 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1725,7 +1725,7 @@ let declare_instance a aeq n s = declare_an_instance n s [a;aeq] let anew_instance global binders instance fields = new_instance (Flags.is_universe_polymorphism ()) binders instance (Some (true, CRecord (Loc.ghost,None,fields))) - ~global ~generalize:false None + ~global ~generalize:false ~refine:false None let declare_instance_refl global binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive" diff --git a/test-suite/bugs/closed/2848.v b/test-suite/bugs/closed/2848.v index de137d39d1..828e3b8c1f 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 diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 5f73b70a2e..653b4695ce 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -119,7 +119,7 @@ let declare_instance_constant k pri global imps ?hook id pl poly evm term termty instance_hook k pri global imps ?hook (ConstRef kn); id -let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) props +let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) poly ctx (instid, bk, cl) props ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri = let env = Global.env() in @@ -290,7 +290,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro if not (Evd.has_undefined evm) && not (Option.is_empty term) then declare_instance_constant k pri global imps ?hook id pl poly evm (Option.get term) termtype - else if Flags.is_program_mode () || !refine_instance || Option.is_empty term then begin + else if Flags.is_program_mode () || refine || Option.is_empty term then begin let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in if Flags.is_program_mode () then let hook vis gr _ = diff --git a/toplevel/classes.mli b/toplevel/classes.mli index d600b3104f..f51e70388e 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -41,6 +41,7 @@ val declare_instance_constant : val new_instance : ?abstract:bool -> (** Not abstract by default. *) ?global:bool -> (** Not global by default. *) + ?refine:bool -> (** Allow refinement *) Decl_kinds.polymorphic -> local_binder list -> typeclass_constraint -> |