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
---
 plugins/cc/cctac.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/cc')

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 73c050bb20..70aaa0c0fc 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -65,7 +65,7 @@ let rec decompose_term env sigma t=
 	let canon_mind = mind_of_kn (canonical_mind mind) in
 	let canon_ind = canon_mind,i_ind in
 	let (oib,_)=Global.lookup_inductive (canon_ind) in
-	let nargs=mis_constructor_nargs_env env (canon_ind,i_con) in
+	let nargs=constructor_nallargs_env env (canon_ind,i_con) in
 	  Constructor {ci_constr= ((canon_ind,i_con),u);
 		       ci_arity=nargs;
 		       ci_nhyps=nargs-oib.mind_nparams}
-- 
cgit v1.2.3