diff options
Diffstat (limited to 'pretyping/inductiveops.ml')
| -rw-r--r-- | pretyping/inductiveops.ml | 43 |
1 files changed, 31 insertions, 12 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index e180c13465..07dacd0ccc 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -307,7 +307,7 @@ let make_arity_signature env dep indf = let (arsign,_) = get_arity env indf in if dep then (* We need names everywhere *) - name_context env + Namegen.name_context env ((Anonymous,None,build_dependent_inductive env indf)::arsign) (* Costly: would be better to name once for all at definition time *) else @@ -320,7 +320,7 @@ let make_arity env dep indf s = mkArity (make_arity_signature env dep indf, s) let build_branch_type env dep p cs = let base = appvect (lift cs.cs_nargs p, cs.cs_concl_realargs) in if dep then - it_mkProd_or_LetIn_name env + Namegen.it_mkProd_or_LetIn_name env (applist (base,[build_dependent_constructor cs])) cs.cs_args else @@ -371,13 +371,28 @@ let find_coinductive env sigma c = (* find appropriate names for pattern variables. Useful in the Case and Inversion (case_then_using et case_nodep_then_using) tactics. *) +let h_based_elimination_names = ref true + +let use_h_based_elimination_names () = + !h_based_elimination_names && Flags.version_strictly_greater Flags.V8_4 + +open Goptions + +let _ = declare_bool_option + { optsync = true; + optdepr = false; + optname = "use of \"H\"-based proposition names in elimination tactics"; + optkey = ["Standard";"Proposition";"Elimination";"Names"]; + optread = (fun () -> !h_based_elimination_names); + optwrite = (:=) h_based_elimination_names } + let is_predicate_explicitly_dep env pred arsign = let rec srec env pval arsign = let pv' = whd_betadeltaiota env Evd.empty pval in match kind_of_term pv', arsign with | Lambda (na,t,b), (_,None,_)::arsign -> srec (push_rel_assum (na,t) env) b arsign - | Lambda (na,_,_), _ -> + | Lambda (na,_,t), _ -> (* The following code has an impact on the introduction names given by the tactics "case" and "inversion": when the @@ -396,10 +411,12 @@ let is_predicate_explicitly_dep env pred arsign = dependency status (of course, Anonymous implies non dependent, but not conversely). - At the end, this is only to preserve the compatibility: a - check whether the predicate is actually dependent or not - would indeed be more natural! *) + From Coq > 8.2, using or not the the effective dependency of + the predicate is parametrable! *) + if use_h_based_elimination_names () then + dependent (mkRel 1) t + else begin match na with | Anonymous -> false | Name _ -> true @@ -413,11 +430,13 @@ let is_elim_predicate_explicitly_dependent env pred indf = let arsign,_ = get_arity env indf in is_predicate_explicitly_dep env pred arsign -let set_names env n brty = +let set_names preprocess_names env n brty = let (ctxt,cl) = decompose_prod_n_assum n brty in - it_mkProd_or_LetIn_name env cl ctxt + let ctxt = + if use_h_based_elimination_names () then preprocess_names ctxt else ctxt in + Namegen.it_mkProd_or_LetIn_name env cl ctxt -let set_pattern_names env ind brv = +let set_pattern_names preprocess_names env ind brv = let (mib,mip) = Inductive.lookup_mind_specif env ind in let arities = Array.map @@ -425,9 +444,9 @@ let set_pattern_names env ind brv = rel_context_length ((prod_assum c)) - mib.mind_nparams) mip.mind_nf_lc in - Array.map2 (set_names env) arities brv + Array.map2 (set_names preprocess_names env) arities brv -let type_case_branches_with_names env indspec p c = +let type_case_branches_with_names preprocess_names env indspec p c = let (ind,args) = indspec in let (mib,mip as specif) = Inductive.lookup_mind_specif env (fst ind) in let nparams = mib.mind_nparams in @@ -437,7 +456,7 @@ let type_case_branches_with_names env indspec p c = let conclty = Reduction.beta_appvect p (Array.of_list (realargs@[c])) in (* Adjust names *) if is_elim_predicate_explicitly_dependent env p (ind,params) then - (set_pattern_names env (fst ind) lbrty, conclty) + (set_pattern_names preprocess_names env (fst ind) lbrty, conclty) else (lbrty, conclty) (* Type of Case predicates *) |