diff options
| author | Matej Kosik | 2015-12-16 16:19:51 +0100 |
|---|---|---|
| committer | Matej Kosik | 2016-01-11 14:59:26 +0100 |
| commit | a1aff01d16bad2f44392fd5cb804092e12e558ed (patch) | |
| tree | bd2a1faf08b1c399171a308cf45bfd46d60ab5c5 /tactics | |
| parent | 78bad016e389cd78635d40281bfefd7136733b7e (diff) | |
CLEANUP: removing unused field
I have removed the second field of the "Constrexpr.CRecord" variant
because once it was set to "None"
it never changed to anything else.
It was just carried and copied around.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/rewrite.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 2dfebc9a3c..eddefb2799 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1710,7 +1710,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))) + binders instance (Some (true, CRecord (Loc.ghost,fields))) ~global ~generalize:false None let declare_instance_refl global binders a aeq n lemma = @@ -1925,7 +1925,7 @@ let add_morphism glob binders m s n = in let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in ignore(new_instance ~global:glob poly binders instance - (Some (true, CRecord (Loc.ghost,None,[]))) + (Some (true, CRecord (Loc.ghost,[]))) ~generalize:false ~tac ~hook:(declare_projection n instance_id) None) (** Bind to "rewrite" too *) |