diff options
| author | Hugo Herbelin | 2014-08-01 14:27:23 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-08-01 14:27:23 +0200 |
| commit | 128a297614d1e0fb32e2bbd465d181c5d5b1562c (patch) | |
| tree | 1677d5a840c68549cf6530caf2929476a85ad68a /dev/doc | |
| 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 'dev/doc')
| -rw-r--r-- | dev/doc/changes.txt | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index a919b86c27..036bf1d5e3 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -85,6 +85,8 @@ renamed into replace_term_occ_modulo and replace_term_occ_decl_modulo). +- API of Inductiveops made more uniform (see commit log or file itself). + ========================================= = CHANGES BETWEEN COQ V8.3 AND COQ V8.4 = ========================================= |