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
---
 interp/constrextern.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'interp/constrextern.ml')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 5ce7f8f91d..9c2f8bcd3f 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -165,7 +165,7 @@ let in_debugger = ref false
 
 let add_patt_for_params ind l =
   if !in_debugger then l else
-    Util.List.addn (fst (Inductiveops.inductive_nargs ind)) (CPatAtom (Loc.ghost,None)) l
+    Util.List.addn (Inductiveops.inductive_nparamdecls ind) (CPatAtom (Loc.ghost,None)) l
 
 let drop_implicits_in_patt cst nb_expl args =
   let impl_st = (implicits_of_global cst) in
@@ -275,7 +275,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
      not explicit application. *)
   match pat with
     | PatCstr(loc,cstrsp,args,na)
-	when !in_debugger||Inductiveops.mis_constructor_has_local_defs cstrsp ->
+	when !in_debugger||Inductiveops.constructor_has_local_defs cstrsp ->
       let c = extern_reference loc Id.Set.empty (ConstructRef cstrsp) in
       let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
       CPatCstr (loc, c, add_patt_for_params (fst cstrsp) args, [])
-- 
cgit v1.2.3