Stronger invariants on the use of the introduction pattern (pat1,...,patn).

The length of the pattern should now be exactly the number of
assumptions and definitions introduced by the destruction or induction,
including the induction hypotheses in case of an induction.

Like for pattern-matching, the local definitions in the argument of
the constructor can be skipped in which case a name is automatically
created for these.

1 files changed, 3 insertions, 3 deletions

diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 56106928e5..2f206bfc84 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 }
                         ]);