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/inv.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/inv.ml')
| -rw-r--r-- | tactics/inv.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tactics/inv.ml b/tactics/inv.ml index 3574990f6..01124e867 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -296,17 +296,17 @@ let get_names (allow_conj,issimple) (loc, pat as x) = match pat with error "Discarding pattern not allowed for inversion equations." | IntroAction (IntroRewrite _) -> error "Rewriting pattern not allowed for inversion equations." - | IntroAction (IntroOrAndPattern [[]]) when allow_conj -> (None, []) - | IntroAction (IntroOrAndPattern [(_,IntroNaming (IntroIdentifier id)) :: _ as l]) + | IntroAction (IntroOrAndPattern (IntroAndPattern [])) when allow_conj -> (None, []) + | IntroAction (IntroOrAndPattern (IntroAndPattern ((_,IntroNaming (IntroIdentifier id)) :: _ as l))) when allow_conj -> (Some id,l) - | IntroAction (IntroOrAndPattern [_]) -> + | IntroAction (IntroOrAndPattern (IntroAndPattern _)) -> if issimple then error"Conjunctive patterns not allowed for simple inversion equations." else error"Nested conjunctive patterns not allowed for inversion equations." | IntroAction (IntroInjection l) -> error "Injection patterns not allowed for inversion equations." - | IntroAction (IntroOrAndPattern l) -> + | IntroAction (IntroOrAndPattern (IntroOrPattern _)) -> error "Disjunctive patterns not allowed for inversion equations." | IntroAction (IntroApplyOn (c,pat)) -> error "Apply patterns not allowed for inversion equations." |