From f9517286637fd0891a3ac1aac041b437e157f756 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 1 Aug 2014 15:02:58 +0200 Subject: 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. --- pretyping/inductiveops.mli | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'pretyping/inductiveops.mli') 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 -- cgit v1.2.3