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 /tactics | |
| 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 'tactics')
| -rw-r--r-- | tactics/rewrite.ml | 2 |
1 files changed, 1 insertions, 1 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" |