diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-01 14:27:23 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-01 14:27:23 +0200 |
| commit | 128a297614d1e0fb32e2bbd465d181c5d5b1562c (patch) | |
| tree | 1677d5a840c68549cf6530caf2929476a85ad68a /checker/declarations.ml | |
| parent | d89eaa87029b05ab79002632e9c375fd877c2941 (diff) | |
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
Diffstat (limited to 'checker/declarations.ml')
| -rw-r--r-- | checker/declarations.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/declarations.ml b/checker/declarations.ml index c705a707f..d38df793f 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -557,7 +557,7 @@ let subst_mind_packet sub mbp = mind_arity = subst_ind_arity sub mbp.mind_arity; mind_user_lc = Array.smartmap (subst_mps sub) mbp.mind_user_lc; mind_nrealargs = mbp.mind_nrealargs; - mind_nrealargs_ctxt = mbp.mind_nrealargs_ctxt; + mind_nrealdecls = mbp.mind_nrealdecls; mind_kelim = mbp.mind_kelim; mind_recargs = subst_wf_paths sub mbp.mind_recargs (*wf_paths*); mind_nb_constant = mbp.mind_nb_constant; |