Making type interning_data abstract in constrintern.ml.

3 files changed, 16 insertions, 10 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 75fda5d239..7431058849 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -186,6 +186,9 @@ let compute_internalization_env env sigma ?(impls=empty_internalization_env) ty
     (fun map id typ impl -> Id.Map.add id (compute_internalization_data env sigma ty typ impl) map)
     impls
 
+let extend_internalization_data (r, impls, scopes) impl scope =
+  (r, impls@[impl], scopes@[scope])
+
 (**********************************************************************)
 (* Contracting "{ _ }" in notations *)
 
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 9f06f16258..efbe7ec910 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -43,13 +43,12 @@ type var_internalization_type =
   | Method
   | Variable
 
-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 *)
-
-    Impargs.implicit_status list * (* signature of impargs of the variable *)
-    Notation_term.scope_name option list (* subscopes of the args of the variable *)
+(** This collects relevant information for interning local variables:
+   - their coqdoc kind (a recursive call in a inductive, fixpoint of class; or a bound variable)
+     e.g. while typing the constructor of JMeq, "JMeq" behaves as a variable of type Inductive
+   - their implicit arguments
+   - their argument scopes *)
+type var_internalization_data
 
 (** A map of free variables to their implicit arguments and scopes *)
 type internalization_env = var_internalization_data Id.Map.t
@@ -63,6 +62,9 @@ val compute_internalization_env : env -> evar_map -> ?impls:internalization_env
   Id.t list -> types list -> Impargs.manual_implicits list ->
   internalization_env
 
+val extend_internalization_data :
+  var_internalization_data -> Impargs.implicit_status -> scope_name option -> var_internalization_data
+
 type ltac_sign = {
   ltac_vars : Id.Set.t;
   (** Variables of Ltac which may be bound to a term *)
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 80e7e6ab96..5b29ab2092 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -195,13 +195,14 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
   let lift_lets = lift_rel_context 1 letbinders in
   let sigma, intern_body =
     let ctx = LocalAssum (make_annot (Name recname) Sorts.Relevant, get_type curry_fun) :: binders_rel in
-    let (r, impls, scopes) =
+    let interning_data =
       Constrintern.compute_internalization_data env sigma
         Constrintern.Recursive full_arity impls
     in
     let newimpls = Id.Map.singleton recname
-        (r, impls @ [Some (ExplByName (Id.of_string "recproof"), Impargs.Manual, (true, false))],
-         scopes @ [None]) in
+        (Constrintern.extend_internalization_data interning_data
+           (Some (ExplByName (Id.of_string "recproof"), Impargs.Manual, (true, false)))
+           None) in
     interp_casted_constr_evars ~program_mode:true (push_rel_context ctx env) sigma
       ~impls:newimpls body (lift 1 top_arity)
   in