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
---
 dev/doc/changes.txt | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'dev/doc')

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 =
 =========================================
-- 
cgit v1.2.3