Simplified the way internalization_data (i.e. bindings of bound vars

to their signature of implicit positions and scopes) is computed.
A bit of documentation in constrintern.mli.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13315 85f007b7-540e-0410-9357-904b9bb8a0f7

9 files changed, 100 insertions, 114 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 81ddb27319..84327add61 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -26,7 +26,10 @@ open Inductiveops
 (* To interpret implicits and arg scopes of variables in inductive
    types and recursive definitions and of projection names in records *)
 
-type var_internalization_type = Inductive | Recursive | Method
+type var_internalization_type =
+  | Inductive of identifier list (* list of params *)
+  | Recursive
+  | Method
 
 type var_internalization_data =
     (* type of the "free" variable, for coqdoc, e.g. while typing the
@@ -43,13 +46,6 @@ type var_internalization_data =
 type internalization_env =
     (identifier * var_internalization_data) list
 
-type full_internalization_env =
-    (* a superset of the list of variables that may be automatically
-       inserted and that must not occur as binders *)
-    identifier list *
-    (* mapping of the variables to their internalization data *)
-    internalization_env
-
 type raw_binder = (name * binding_kind * rawconstr option * rawconstr)
 
 let interning_grammar = ref false
@@ -169,30 +165,26 @@ let error_inductive_parameter_not_implicit loc =
 (* Pre-computing the implicit arguments and arguments scopes needed   *)
 (* for interpretation *)
 
-let empty_internalization_env = ([],[])
+let empty_internalization_env = []
 
-let set_internalization_env_params ienv params =
-  let nparams = List.length params in
-  if nparams = 0 then
-    ([],ienv)
-  else
-    let ienv_with_implicit_params =
-      List.map (fun (id,(ty,_,impl,scopes)) ->
-	let sub_impl,_ = list_chop nparams impl in
-	let sub_impl' = List.filter is_status_implicit sub_impl in
-	(id,(ty,List.map name_of_implicit sub_impl',impl,scopes))) ienv in
-    (params, ienv_with_implicit_params)
-
-let compute_internalization_data env ty typ impls =
-  let impl = compute_implicits_with_manual env typ (is_implicit_args()) impls in
-  (ty, [], impl, compute_arguments_scope typ)
-
-let compute_full_internalization_env env ty params idl typl impll =
-  set_internalization_env_params
-    (list_map3
-      (fun id typ impl -> (id,compute_internalization_data env ty typ impl))
-      idl typl impll)
-    params
+let compute_explicitable_implicit imps = function
+  | Inductive params ->
+      (* In inductive types, the parameters are fixed implicit arguments *)
+      let sub_impl,_ = list_chop (List.length params) imps in
+      let sub_impl' = List.filter is_status_implicit sub_impl in
+      List.map name_of_implicit sub_impl'
+  | Recursive | Method ->
+      (* Unable to know in advance what the implicit arguments will be *)
+      []
+
+let compute_internalization_data env ty typ impl =
+  let impl = compute_implicits_with_manual env typ (is_implicit_args()) impl in
+  let expls_impl = compute_explicitable_implicit impl ty in
+  (ty, expls_impl, impl, compute_arguments_scope typ)
+
+let compute_internalization_env env ty =
+  list_map3
+    (fun id typ impl -> (id,compute_internalization_data env ty typ impl))
 
 (**********************************************************************)
 (* Contracting "{ _ }" in notations *)
@@ -283,9 +275,12 @@ let locate_if_isevar loc na = function
       with Not_found -> RHole (loc, Evd.BinderType na))
   | x -> x
 
-let check_hidden_implicit_parameters id (_,_,_,(indnames,_)) =
-  if List.mem id indnames then
-    errorlabstrm "" (strbrk "A parameter or name of an inductive type " ++
+let check_hidden_implicit_parameters id (_,_,_,impls) =
+  if List.exists (function
+    | (_,(Inductive indparams,_,_,_)) -> List.mem id indparams
+    | _ -> false) impls
+  then
+    errorlabstrm "" (strbrk "A parameter of an inductive type " ++
     pr_id id ++ strbrk " is not allowed to be used as a bound variable in the type of its constructor.")
 
 let push_name_env ?(global_level=false) lvar (ids,unb,tmpsc,scopes as env) =
@@ -461,34 +456,30 @@ let rec it_mkRLambda env body =
 (**********************************************************************)
 (* Discriminating between bound variables and global references       *)
 
-(* [vars1] is a set of name to avoid (used for the tactic language);
-   [vars2] is the set of global variables, env is the set of variables
-   abstracted until this point *)
-
 let string_of_ty = function
-  | Inductive -> "ind"
+  | Inductive _ -> "ind"
   | Recursive -> "def"
   | Method -> "meth"
 
-let intern_var (env,unbound_vars,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) loc id =
-  let (vars1,unbndltacvars) = ltacvars in
+let intern_var (ids,_,_,_ as genv) (ltacvars,namedctxvars,ntnvars,impls) loc id =
+  let (ltacvars,unbndltacvars) = ltacvars in
   (* Is [id] an inductive type potentially with implicit *)
   try
-    let ty,l,impl,argsc = List.assoc id impls in
-    let l = List.map
-      (fun id -> CRef (Ident (loc,id)), Some (loc,ExplByName id)) l in
+    let ty,expl_impls,impls,argsc = List.assoc id impls in
+    let expl_impls = List.map
+      (fun id -> CRef (Ident (loc,id)), Some (loc,ExplByName id)) expl_impls in
     let tys = string_of_ty ty in
-      Dumpglob.dump_reference loc "<>" (string_of_id id) tys;
-      RVar (loc,id), impl, argsc, l
+    Dumpglob.dump_reference loc "<>" (string_of_id id) tys;
+    RVar (loc,id), impls, argsc, expl_impls
   with Not_found ->
-  (* Is [id] bound in current env or is an ltac var bound to constr *)
-  if Idset.mem id env or List.mem id vars1
+  (* Is [id] bound in current term or is an ltac var bound to constr *)
+  if Idset.mem id ids or List.mem id ltacvars
   then
     RVar (loc,id), [], [], []
   (* Is [id] a notation variable *)
-  else if List.mem_assoc id vars3
+  else if List.mem_assoc id ntnvars
   then
-    (set_var_scope loc id genv vars3; RVar (loc,id), [], [], [])
+    (set_var_scope loc id genv ntnvars; RVar (loc,id), [], [], [])
   else
   (* Is [id] bound to a free name in ltac (this is an ltac error message) *)
   try
@@ -498,7 +489,7 @@ let intern_var (env,unbound_vars,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) l
       | Some id0 -> Pretype_errors.error_var_not_found_loc loc id0
   with Not_found ->
     (* Is [id] a goal or section variable *)
-    let _ = Sign.lookup_named id vars2 in
+    let _ = Sign.lookup_named id namedctxvars in
       try
 	(* [id] a section variable *)
 	(* Redundant: could be done in intern_qualid *)
@@ -582,7 +573,7 @@ let intern_applied_reference intern (_, unb, _, _ as env) lvar args = function
 let interp_reference vars r =
   let (r,_,_,_),_ =
     intern_applied_reference (fun _ -> error_not_enough_arguments dummy_loc)
-      (Idset.empty,false,None,[]) (vars,[],[],([],[])) [] r
+      (Idset.empty,false,None,[]) (vars,[],[],[]) [] r
   in r
 
 let apply_scope_env (ids,unb,_,scopes) = function
@@ -1348,7 +1339,7 @@ let extract_ids env =
     Idset.empty
 
 let intern_gen isarity sigma env
-               ?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[]))
+               ?(impls=[]) ?(allow_patvar=false) ?(ltacvars=([],[]))
                c =
   let tmp_scope =
     if isarity then Some Notation.type_scope else None in
@@ -1373,7 +1364,7 @@ type manual_implicits = (explicitation * (bool * bool * bool)) list
 (* Functions to parse and interpret constructions *)
 
 let interp_gen kind sigma env
-               ?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[]))
+               ?(impls=[]) ?(allow_patvar=false) ?(ltacvars=([],[]))
                c =
   let c = intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars sigma env c in
     Default.understand_gen kind sigma env c
@@ -1381,10 +1372,10 @@ let interp_gen kind sigma env
 let interp_constr sigma env c =
   interp_gen (OfType None) sigma env c
 
-let interp_type sigma env ?(impls=([],[])) c =
+let interp_type sigma env ?(impls=[]) c =
   interp_gen IsType sigma env ~impls c
 
-let interp_casted_constr sigma env ?(impls=([],[])) c typ =
+let interp_casted_constr sigma env ?(impls=[]) c typ =
   interp_gen (OfType (Some typ)) sigma env ~impls c
 
 let interp_open_constr sigma env c =
@@ -1412,7 +1403,7 @@ let interp_constr_judgment sigma env c =
   Default.understand_judgment sigma env (intern_constr sigma env c)
 
 let interp_constr_evars_gen_impls ?evdref ?(fail_evar=true)
-    env ?(impls=([],[])) kind c =
+    env ?(impls=[]) kind c =
   let evdref =
     match evdref with
     | None -> ref Evd.empty
@@ -1424,23 +1415,23 @@ let interp_constr_evars_gen_impls ?evdref ?(fail_evar=true)
     Default.understand_tcc_evars ~fail_evar evdref env kind c, imps
 
 let interp_casted_constr_evars_impls ?evdref ?(fail_evar=true)
-    env ?(impls=([],[])) c typ =
+    env ?(impls=[]) c typ =
   interp_constr_evars_gen_impls ?evdref ~fail_evar env ~impls (OfType (Some typ)) c
 
-let interp_type_evars_impls ?evdref ?(fail_evar=true) env ?(impls=([],[])) c =
+let interp_type_evars_impls ?evdref ?(fail_evar=true) env ?(impls=[]) c =
   interp_constr_evars_gen_impls ?evdref ~fail_evar env IsType ~impls c
 
-let interp_constr_evars_impls ?evdref ?(fail_evar=true) env ?(impls=([],[])) c =
+let interp_constr_evars_impls ?evdref ?(fail_evar=true) env ?(impls=[]) c =
   interp_constr_evars_gen_impls ?evdref ~fail_evar env (OfType None) ~impls c
 
-let interp_constr_evars_gen evdref env ?(impls=([],[])) kind c =
+let interp_constr_evars_gen evdref env ?(impls=[]) kind c =
   let c = intern_gen (kind=IsType) ~impls ( !evdref) env c in
     Default.understand_tcc_evars evdref env kind c
 
-let interp_casted_constr_evars evdref env ?(impls=([],[])) c typ =
+let interp_casted_constr_evars evdref env ?(impls=[]) c typ =
   interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c
 
-let interp_type_evars evdref env ?(impls=([],[])) c =
+let interp_type_evars evdref env ?(impls=[]) c =
   interp_constr_evars_gen evdref env IsType ~impls c
 
 type ltac_sign = identifier list * unbound_ltac_var_map
@@ -1449,7 +1440,7 @@ let intern_constr_pattern sigma env ?(as_type=false) ?(ltacvars=([],[])) c =
   let c = intern_gen as_type ~allow_patvar:true ~ltacvars sigma env c in
   pattern_of_rawconstr c
 
-let interp_aconstr ?(impls=([],[])) (vars,varslist) a =
+let interp_aconstr ?(impls=[]) (vars,varslist) a =
   let env = Global.env () in
   (* [vl] is intended to remember the scope of the free variables of [a] *)
   let vl = List.map (fun id -> (id,ref None)) (vars@varslist) in
@@ -1484,7 +1475,7 @@ let my_intern_constr sigma env lvar acc c =
 let my_intern_type sigma env lvar acc c = my_intern_constr sigma env lvar (set_type_scope acc) c
 
 let intern_context global_level sigma env params =
-  let lvar = (([],[]),Environ.named_context env, [], ([], [])) in
+  let lvar = (([],[]),Environ.named_context env, [], []) in
     snd (List.fold_left
 	    (intern_local_binder_aux ~global_level (my_intern_constr sigma env lvar) (my_intern_type sigma env lvar) lvar)
 	    ((extract_ids env,false,None,[]), []) params)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 1dd221f69b..e1f1c50b46 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -26,44 +26,43 @@ open Pretyping
       - check all variables are bound
       - make absolute the references to global objets
    - resolution of symbolic notations using scopes
-   - insert existential variables for implicit arguments
+   - insertion of implicit arguments
 
-   To interpret implicits and arg scopes of recursive variables while
-   internalizing inductive types and recursive definitions, and also
+   To interpret implicit arguments and arg scopes of recursive variables
+   while internalizing inductive types and recursive definitions, and also
    projection while typing records.
 
    the third and fourth arguments associate a list of implicit
    positions and scopes to identifiers declared in the [rel_context]
    of [env] *)
 
-type var_internalization_type = Inductive | Recursive | Method
+type var_internalization_type =
+  | Inductive of identifier list (* list of params *)
+  | Recursive
+  | Method
 
 type var_internalization_data =
     var_internalization_type *
+      (** type of the "free" variable, for coqdoc, e.g. while typing the
+	  constructor of JMeq, "JMeq" behaves as a variable of type Inductive *)
     identifier list *
-    Impargs.implicits_list *
-    scope_name option list
+      (** impargs to automatically add to the variable, e.g. for "JMeq A a B b"
+          in implicit mode, this is [A;B] and this adds (A:=A) and (B:=B) *)
+    Impargs.implicits_list * (** signature of impargs of the variable *)
+    scope_name option list (** subscopes of the args of the variable *)
 
 (** A map of free variables to their implicit arguments and scopes *)
 type internalization_env =
     (identifier * var_internalization_data) list
 
-(** Contains also a list of identifiers to automatically apply to the variables*)
-type full_internalization_env =
-    identifier list * internalization_env
-
-val empty_internalization_env : full_internalization_env
+val empty_internalization_env : internalization_env
 
 val compute_internalization_data : env -> var_internalization_type ->
   types -> Impargs.manual_explicitation list -> var_internalization_data
 
-val set_internalization_env_params :
-  internalization_env -> identifier list -> full_internalization_env
-
-val compute_full_internalization_env : env ->
-  var_internalization_type ->
-  identifier list -> identifier list -> types list ->
-  Impargs.manual_explicitation list list -> full_internalization_env
+val compute_internalization_env : env -> var_internalization_type ->
+  identifier list -> types list -> Impargs.manual_explicitation list list ->
+  internalization_env
 
 type manual_implicits = (explicitation * (bool * bool * bool)) list
 
@@ -78,7 +77,7 @@ val intern_constr : evar_map -> env -> constr_expr -> rawconstr
 val intern_type : evar_map -> env -> constr_expr -> rawconstr
 
 val intern_gen : bool -> evar_map -> env ->
-  ?impls:full_internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
+  ?impls:internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
   constr_expr -> rawconstr
 
 val intern_pattern : env -> cases_pattern_expr ->
@@ -92,7 +91,7 @@ val intern_context : bool -> evar_map -> env -> local_binder list -> raw_binder
 (** Main interpretation function *)
 
 val interp_gen : typing_constraint -> evar_map -> env ->
-  ?impls:full_internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
+  ?impls:internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
   constr_expr -> constr
 
 (** Particular instances *)
@@ -100,33 +99,33 @@ val interp_gen : typing_constraint -> evar_map -> env ->
 val interp_constr : evar_map -> env ->
   constr_expr -> constr
 
-val interp_type : evar_map -> env -> ?impls:full_internalization_env ->
+val interp_type : evar_map -> env -> ?impls:internalization_env ->
   constr_expr -> types
 
 val interp_open_constr   : evar_map -> env -> constr_expr -> evar_map * constr
 
 val interp_open_constr_patvar   : evar_map -> env -> constr_expr -> evar_map * constr
 
-val interp_casted_constr : evar_map -> env -> ?impls:full_internalization_env ->
+val interp_casted_constr : evar_map -> env -> ?impls:internalization_env ->
   constr_expr -> types -> constr
 
 (** Accepting evars and giving back the manual implicits in addition. *)
 
 val interp_casted_constr_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool -> env ->
-  ?impls:full_internalization_env -> constr_expr -> types -> constr * manual_implicits
+  ?impls:internalization_env -> constr_expr -> types -> constr * manual_implicits
 
 val interp_type_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool ->
-  env -> ?impls:full_internalization_env ->
+  env -> ?impls:internalization_env ->
   constr_expr -> types * manual_implicits
 
 val interp_constr_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool ->
-  env -> ?impls:full_internalization_env ->
+  env -> ?impls:internalization_env ->
   constr_expr -> constr * manual_implicits
 
 val interp_casted_constr_evars : evar_map ref -> env ->
-  ?impls:full_internalization_env -> constr_expr -> types -> constr
+  ?impls:internalization_env -> constr_expr -> types -> constr
 
-val interp_type_evars : evar_map ref -> env -> ?impls:full_internalization_env ->
+val interp_type_evars : evar_map ref -> env -> ?impls:internalization_env ->
   constr_expr -> types
 
 (** {6 Build a judgment  } *)
@@ -174,7 +173,7 @@ val global_reference_in_absolute_module : dir_path -> identifier -> constr
 
 (** Interprets into a abbreviatable constr *)
 
-val interp_aconstr : ?impls:full_internalization_env ->
+val interp_aconstr : ?impls:internalization_env ->
   identifier list * identifier list -> constr_expr -> interpretation
 
 (** Globalization leak for Grammar *)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index b2acea2373..ba9bde01c8 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -152,9 +152,8 @@ let build_newrecursive
         let arityc = Topconstr.prod_constr_expr arityc bl in
         let arity = Constrintern.interp_type sigma env0 arityc in
 	let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity [] in
-        (Environ.push_named (recname,None,arity) env, (recname,impl) :: impls))
+        (Environ.push_named (recname,None,arity) env, (recname, impl) :: impls))
       (env0,[]) lnameargsardef in
-  let rec_impls = Constrintern.set_internalization_env_params rec_impls [] in
   let recdef =
     (* Declare local notations *)
     let fs = States.freeze() in
diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index 2fe22364d5..3c04dd9ca6 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -27,11 +27,11 @@ open Util
 
 module SPretyping = Subtac_pretyping.Pretyping
 
-let interp_constr_evars_gen evdref env ?(impls=([],[])) kind c =
+let interp_constr_evars_gen evdref env ?(impls=[]) kind c =
   SPretyping.understand_tcc_evars evdref env kind
     (intern_gen (kind=IsType) ~impls ( !evdref) env c)
 
-let interp_casted_constr_evars evdref env ?(impls=([],[])) c typ =
+let interp_casted_constr_evars evdref env ?(impls=[]) c typ =
   interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c
 
 let interp_context_evars evdref env params =
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index 0027cb1ffe..634a6ea600 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -53,7 +53,7 @@ let evar_nf isevars c =
   Evarutil.nf_evar !isevars c
 
 let interp_gen kind isevars env
-               ?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[]))
+               ?(impls=[]) ?(allow_patvar=false) ?(ltacvars=([],[]))
                c =
   let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars ( !isevars) env c in
   let c' = SPretyping.understand_tcc_evars isevars env kind c' in
@@ -62,13 +62,13 @@ let interp_gen kind isevars env
 let interp_constr isevars env c =
   interp_gen (OfType None) isevars env c
 
-let interp_type_evars isevars env ?(impls=([],[])) c =
+let interp_type_evars isevars env ?(impls=[]) c =
   interp_gen IsType isevars env ~impls c
 
-let interp_casted_constr isevars env ?(impls=([],[])) c typ =
+let interp_casted_constr isevars env ?(impls=[]) c typ =
   interp_gen (OfType (Some typ)) isevars env ~impls c
 
-let interp_casted_constr_evars isevars env ?(impls=([],[])) c typ =
+let interp_casted_constr_evars isevars env ?(impls=[]) c typ =
   interp_gen (OfType (Some typ)) isevars env ~impls c
 
 let interp_open_constr isevars env c =
@@ -296,14 +296,13 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
   let lift_lets = Termops.lift_rel_context 1 letbinders in
   let intern_body =
     let ctx = (Name recname, None, pi3 curry_fun) :: binders_rel in
-    let (r, l, impls, scopes) = 
+    let (r, l, impls, scopes) =
       Constrintern.compute_internalization_data env
 	Constrintern.Recursive full_arity impls 
     in
     let newimpls = [(recname, (r, l, impls @ 
       [Some (id_of_string "recproof", Impargs.Manual, (true, false))], 
 			      scopes @ [None]))] in
-    let newimpls = Constrintern.set_internalization_env_params newimpls [] in
     interp_casted_constr isevars ~impls:newimpls
       (push_rel_context ctx env) body (lift 1 top_arity)
   in
@@ -442,8 +441,8 @@ let interp_recursive fixkind l boxed =
   let env_rec = push_named_context rec_sign env in
 
   (* Get interpretation metadatas *)
-  let impls = Constrintern.compute_full_internalization_env env 
-    Constrintern.Recursive [] fixnames fixtypes fiximps 
+  let impls = Constrintern.compute_internalization_env env
+    Constrintern.Recursive fixnames fixtypes fiximps
   in
   let notations = List.flatten ntnl in
 
diff --git a/plugins/subtac/subtac_command.mli b/plugins/subtac/subtac_command.mli
index 304aa139e2..0f24915e30 100644
--- a/plugins/subtac/subtac_command.mli
+++ b/plugins/subtac/subtac_command.mli
@@ -13,7 +13,7 @@ val interp_gen :
   typing_constraint ->
   evar_map ref ->
   env ->
-  ?impls:full_internalization_env ->
+  ?impls:internalization_env ->
   ?allow_patvar:bool ->
   ?ltacvars:ltac_sign ->
   constr_expr -> constr
@@ -23,12 +23,12 @@ val interp_constr :
 val interp_type_evars :
   evar_map ref ->
   env ->
-  ?impls:full_internalization_env ->
+  ?impls:internalization_env ->
   constr_expr -> constr
 val interp_casted_constr_evars :
   evar_map ref ->
   env ->
-  ?impls:full_internalization_env ->
+  ?impls:internalization_env ->
   constr_expr -> types -> constr
 val interp_open_constr :
   evar_map ref -> env -> constr_expr -> constr
diff --git a/toplevel/command.ml b/toplevel/command.ml
index a16afa86ce..d71e586556 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -241,7 +241,7 @@ let interp_mutual_inductive (paramsl,indl) notations finite =
   (* Compute interpretation metadatas *)
   let indimpls = List.map (fun (_, impls) -> userimpls @ lift_implicits (List.length userimpls) impls) arities in
   let arities = List.map fst arities in
-  let impls = compute_full_internalization_env env0 Inductive params indnames fullarities indimpls in
+  let impls = compute_internalization_env env0 (Inductive params) indnames fullarities indimpls in
   let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in
 
   let constructors =
@@ -516,7 +516,7 @@ let interp_recursive isfix fixl notations =
   let env_rec = push_named_types env fixnames fixtypes in
 
   (* Get interpretation metadatas *)
-  let impls = compute_full_internalization_env env Recursive [] fixnames fixtypes fiximps in
+  let impls = compute_internalization_env env Recursive fixnames fixtypes fiximps in
 
   (* Interp bodies with rollback because temp use of notations/implicit *)
   let fixdefs =
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index 216d033819..44e7133e29 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -43,7 +43,7 @@ val add_notation_interpretation :
 
 (** Add a notation interpretation for supporting the "where" clause *)
 
-val set_notation_for_interpretation : Constrintern.full_internalization_env ->
+val set_notation_for_interpretation : Constrintern.internalization_env ->
   (lstring * constr_expr * scope_name option) -> unit
 
 (** Add only the parsing/printing rule of a notation *)
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 12843da60d..5107ee2ac1 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -30,7 +30,6 @@ open Topconstr
 (********** definition d'un record (structure) **************)
 
 let interp_evars evdref env impls k typ =
-  let impls = set_internalization_env_params impls [] in
   let typ' = intern_gen true ~impls !evdref env typ in
   let imps = Implicit_quantifiers.implicits_of_rawterm typ' in
     imps, Pretyping.Default.understand_tcc_evars evdref env k typ'
@@ -46,8 +45,7 @@ let interp_fields_evars evars env nots l =
 	| Name id -> (id, compute_internalization_data env Constrintern.Method t' impl) :: impls
       in
       let d = (i,b',t') in
-      let impls' = set_internalization_env_params impls [] in
-      List.iter (Metasyntax.set_notation_for_interpretation impls') no;
+      List.iter (Metasyntax.set_notation_for_interpretation impls) no;
       (push_rel d env, impl :: uimpls, d::params, impls))
     (env, [], [], []) nots l