diff options
Diffstat (limited to 'toplevel/auto_ind_decl.ml')
| -rw-r--r-- | toplevel/auto_ind_decl.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 56106928e..2f206bfc8 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -85,7 +85,7 @@ let destruct_on c = destruct false None c None None let destruct_on_using c id = destruct false None c - (Some (dl,[[dl,IntroNaming IntroAnonymous]; + (Some (dl,IntroOrPattern [[dl,IntroNaming IntroAnonymous]; [dl,IntroNaming (IntroIdentifier id)]])) None @@ -589,8 +589,8 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). Simple.apply_in freshz (andb_prop()); Proofview.Goal.nf_enter { enter = begin fun gl -> let fresht = fresh_id (Id.of_string "Z") gl in - (destruct_on_as (mkVar freshz) - [[dl,IntroNaming (IntroIdentifier fresht); + destruct_on_as (mkVar freshz) + (IntroOrPattern [[dl,IntroNaming (IntroIdentifier fresht); dl,IntroNaming (IntroIdentifier freshz)]]) end } ]); |