diff options
| author | Matthieu Sozeau | 2016-04-07 15:50:26 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-04-07 20:12:09 +0200 |
| commit | 9f0a896536e709880de5ba638069dea680803f62 (patch) | |
| tree | 5cb3cbc5e54ed4e1037e854949a38a387a20c0b1 | |
| 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.
| -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 -> |