diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-01-21 01:43:10 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-01-21 09:29:26 +0100 |
| commit | 9c2662eecc398f38be3b6280a8f760cc439bc31c (patch) | |
| tree | 497b1c250e3cb2e918982b25bb029c14603ac96f /tactics/tacintern.ml | |
| parent | 4b075af747f65bcd73ff1c78417cf77edf6fbd76 (diff) | |
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.
Diffstat (limited to 'tactics/tacintern.ml')
| -rw-r--r-- | tactics/tacintern.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 14e0fed31..f92213da8 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -258,8 +258,11 @@ and intern_intro_pattern_action lf ist = function | IntroApplyOn (c,pat) -> IntroApplyOn (intern_constr ist c, intern_intro_pattern lf ist pat) -and intern_or_and_intro_pattern lf ist = - List.map (List.map (intern_intro_pattern lf ist)) +and intern_or_and_intro_pattern lf ist = function + | IntroAndPattern l -> + IntroAndPattern (List.map (intern_intro_pattern lf ist) l) + | IntroOrPattern ll -> + IntroOrPattern (List.map (List.map (intern_intro_pattern lf ist)) ll) let intern_or_and_intro_pattern_loc lf ist = function | ArgVar (_,id) as x -> |