From 128a297614d1e0fb32e2bbd465d181c5d5b1562c Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 1 Aug 2014 14:27:23 +0200 Subject: A tentative uniform naming policy in module Inductiveops. - realargs: refers either to the indices of an inductive, or to the proper args of a constructor - params: refers to parameters (which are common to inductive and constructors) - allargs = params + realargs - realdecls: refers to the defining context of indices or proper args of a constructor (it includes letins) - paramdecls: refers to the defining context of params (it includes letins) - alldecls = paramdecls + realdecls --- checker/inductive.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'checker/inductive.ml') diff --git a/checker/inductive.ml b/checker/inductive.ml index 9d739b04c..f6cc5c565 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -59,7 +59,7 @@ let make_inductive_subst mib u = Univ.make_universe_subst u mib.mind_universes else Univ.empty_level_subst -let inductive_params_ctxt (mib,u) = +let inductive_paramdecls (mib,u) = let subst = make_inductive_subst mib u in subst_univs_level_context subst mib.mind_params_ctxt @@ -361,10 +361,10 @@ let extended_rel_list n hyps = reln [] 1 hyps let build_dependent_inductive ind (_,mip) params = - let realargs,_ = List.chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in + let realargs,_ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in applist (Ind ind, - List.map (lift mip.mind_nrealargs_ctxt) params + List.map (lift mip.mind_nrealdecls) params @ extended_rel_list 0 realargs) (* This exception is local *) -- cgit v1.2.3