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

(limited to 'plugins/funind')

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