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 /plugins/funind/recdef_plugin.mllib | |
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 'plugins/funind/recdef_plugin.mllib')
0 files changed, 0 insertions, 0 deletions