diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-13 18:02:11 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-18 18:56:38 +0200 |
commit | 5c82bcd1f87cc893319f2553c81a73c69b13b54d (patch) | |
tree | 83ca001f700b5fdb48d0fac8e249c08c589a1d15 /toplevel | |
parent | d5fece25d8964d5d9fcd55b66164286aeef5fb9f (diff) |
Reorganisation of intropattern code
- emphasizing the different kinds of patterns
- factorizing code of the non-naming intro-patterns
Still some questions:
- Should -> and <- apply to hypotheses or not (currently they apply to
hypotheses either when used in assert-style tactics or apply in, or
when the term to rewrite is a variable, in which case "subst" is
applied)?
- Should "subst" be used when the -> or <- rewrites an equation x=t
posed by "assert" (i.e. rewrite everywhere and clearing x and hyp)?
- Should -> and <- be applicable in non assert-style if the lemma has
quantifications?
Diffstat (limited to 'toplevel')
-rw-r--r-- | toplevel/auto_ind_decl.ml | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index c3dc8f89d..948a726b8 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -86,9 +86,8 @@ let destruct_on_using c id = destruct false [None,Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))] None - (None,Some (dl,IntroOrAndPattern [ - [dl,IntroAnonymous]; - [dl,IntroIdentifier id]])) + (None,Some (dl,[[dl,IntroNaming IntroAnonymous]; + [dl,IntroNaming (IntroIdentifier id)]])) None let destruct_on c = @@ -595,9 +594,9 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). (destruct false [None,Tacexpr.ElimOnConstr (Evd.empty,((mkVar freshz,NoBindings)))] None - (None, Some (dl,IntroOrAndPattern [[ - dl,IntroIdentifier fresht; - dl,IntroIdentifier freshz]])) None) + (None, Some (dl,[[ + dl,IntroNaming (IntroIdentifier fresht); + dl,IntroNaming (IntroIdentifier freshz)]])) None) end ]); (* |