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 +-
 plugins/extraction/extraction.ml        | 2 +-
 plugins/funind/glob_term_to_relation.ml | 4 ++--
 plugins/funind/glob_termops.ml          | 2 +-
 4 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'plugins')

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}
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index cce6aff287..618717cdeb 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -793,7 +793,7 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) u args =
 and extract_case env mle ((kn,i) as ip,c,br) mlt =
   (* [br]: bodies of each branch (in functional form) *)
   (* [ni]: number of arguments without parameters in each branch *)
-  let ni = mis_constr_nargs_env env ip in
+  let ni = constructors_nrealargs_env env ip in
   let br_size = Array.length br in
   assert (Int.equal (Array.length ni) br_size);
   if Int.equal br_size 0 then begin
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 41970fce83..40abdb68b5 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -304,7 +304,7 @@ let build_constructors_of_type ind' argl =
 		  Impargs.implicits_of_global constructref
 		in
 		let cst_narg =
-		  Inductiveops.mis_constructor_nargs_env
+		  Inductiveops.constructor_nallargs_env
 		    (Global.env ())
 		    construct
 		in
@@ -388,7 +388,7 @@ let rec pattern_to_term_and_type env typ  = function
 	mkGVar id
   | PatCstr(loc,constr,patternl,_) ->
       let cst_narg =
-	Inductiveops.mis_constructor_nargs_env
+	Inductiveops.constructor_nallargs_env
 	  (Global.env ())
 	  constr
       in
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 5efaf7954e..4cdea414eb 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -427,7 +427,7 @@ let rec pattern_to_term  = function
 	mkGVar id
   | PatCstr(loc,constr,patternl,_) ->
       let cst_narg =
-	Inductiveops.mis_constructor_nargs_env
+	Inductiveops.constructor_nallargs_env
 	  (Global.env ())
 	  constr
       in
-- 
cgit v1.2.3