Making type interning_data abstract in constrintern.ml.

1 files changed, 9 insertions, 7 deletions

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 *)