diff options
Diffstat (limited to 'toplevel/auto_ind_decl.ml')
| -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 c3dc8f89db..948a726b8c 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 ]); (* |