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 /proofs/logic.ml | |
| 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 'proofs/logic.ml')
| -rw-r--r-- | proofs/logic.ml | 11 |
1 files changed, 1 insertions, 10 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index e1cbe4af0..59de85901 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -314,14 +314,6 @@ let rename_hyp id1 id2 sign = (**********************************************************************) -let name_prop_vars env sigma ctxt = - List.map2 (fun (na,b,t as d) s -> - if na = Anonymous && s = prop_sort then - let s = match Namegen.head_name t with Some id -> string_of_id id | None -> "" in - (Name (add_suffix Namegen.default_prop_ident s),b,t) - else - d) - ctxt (sorts_of_context env sigma ctxt) (************************************************************************) (************************************************************************) @@ -526,8 +518,7 @@ and mk_casegoals sigma goal goalacc p c = let indspec = try Tacred.find_hnf_rectype env sigma ct with Not_found -> anomaly (Pp.str "mk_casegoals") in - let (lbrty,conclty) = - type_case_branches_with_names (name_prop_vars env sigma) env indspec p c in + let (lbrty,conclty) = type_case_branches_with_names env indspec p c in (acc'',lbrty,conclty,sigma,p',c') |