diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-01 15:02:58 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-05 19:52:20 +0200 |
| commit | f9517286637fd0891a3ac1aac041b437e157f756 (patch) | |
| tree | 5ed17f6578b2cf3d2e1f78ee5b75a1022909882c /plugins | |
| parent | 99be46eb50213d1f35dfc4d30f35760ad5e75621 (diff) | |
A new step in the new "standard" naming policy for propositional hypotheses
obtained from case analysis or induction. Made it under experimental status.
This replaces commit bf7d2a3ad2535e7d57db79c17c81aaf67d956965 which was
acting at the level of logic.ml. Now acting in tactics.ml.
Parts of things to be done about naming (not related to Propositions):
induction on H:nat+bool produces hypotheses n and b but destruct on H
produces a and b. This is because induction takes the dependent scheme
whose names are statically inferred to be a and b while destruct
dynamically builds a new scheme.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions