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 /pretyping/inductiveops.mli | |
| 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 'pretyping/inductiveops.mli')
| -rw-r--r-- | pretyping/inductiveops.mli | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 5583eff4d..1561cf97b 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -156,8 +156,7 @@ val arity_of_case_predicate : env -> inductive_family -> bool -> sorts -> types val type_case_branches_with_names : - (rel_context -> rel_context) -> env -> pinductive * constr list -> constr -> - constr -> types array * types + env -> pinductive * constr list -> constr -> constr -> types array * types (** Annotation for cases *) val make_case_info : env -> inductive -> case_style -> case_info |