Small convenient code factorization in constrintern.ml.

No change of semantics.

1 files changed, 11 insertions, 11 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 45255609e0..75fda5d239 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -341,7 +341,7 @@ let impls_binder_list =
 let impls_type_list n ?(args = []) =
   let rec aux acc n c = match DAst.get c with
     | GProd (na,bk,_,c) -> aux (build_impls n bk na acc) (n+1) c
-    | _ -> (Variable,List.rev acc,[])
+    | _ -> List.rev acc
   in aux args n
 
 let impls_term_list n ?(args = []) =
@@ -351,7 +351,7 @@ let impls_term_list n ?(args = []) =
        let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in
        let n,acc' = List.fold_left (fun (n,acc) (na, bk, _, _) -> (n+1,build_impls n bk na acc)) (n,acc) args.(nb) in
        aux acc' n bds.(nb)
-    |_ -> (Variable,List.rev acc,[])
+    |_ -> List.rev acc
   in aux args n
 
 (* Check if in binder "(x1 x2 .. xn : t)", none of x1 .. xn-1 occurs in t *)
@@ -432,7 +432,7 @@ let push_name_env ntnvars implargs env =
         then error_ldots_var ?loc;
       set_var_scope ?loc id false (env.tmp_scope,env.scopes) ntnvars;
       Dumpglob.dump_binding ?loc id;
-      pure_push_name_env (id,implargs) env
+      pure_push_name_env (id,(Variable,implargs,[])) env
 
 let remember_binders_impargs env bl =
   List.map_filter (fun (na,_,_,_) ->
@@ -463,7 +463,7 @@ let intern_generalized_binder intern_type ntnvars
   let ty' = intern_type {env with ids = ids; unb = true} ty in
   let fvs = Implicit_quantifiers.generalizable_vars_of_glob_constr ~bound:ids ~allowed:ids' ty' in
   let env' = List.fold_left
-    (fun env {loc;v=x} -> push_name_env ntnvars (Variable,[],[])(*?*) env (make ?loc @@ Name x))
+    (fun env {loc;v=x} -> push_name_env ntnvars [](*?*) env (make ?loc @@ Name x))
     env fvs in
   let b' = check_implicit_meaningful ?loc b' env in
   let bl = List.map
@@ -530,7 +530,7 @@ let intern_cases_pattern_as_binder ?loc ntnvars env p =
       user_err ?loc (str "Unsupported nested \"as\" clause.");
     il,disjpat
   in
-  let env = List.fold_right (fun {loc;v=id} env -> push_name_env ntnvars (Variable,[],[]) env (make ?loc @@ Name id)) il env in
+  let env = List.fold_right (fun {loc;v=id} env -> push_name_env ntnvars [] env (make ?loc @@ Name id)) il env in
   let na = alias_of_pat (List.hd disjpat) in
   let ienv = Name.fold_right Id.Set.remove na env.ids in
   let id = Namegen.next_name_away_with_default "pat" na ienv in
@@ -586,7 +586,7 @@ let intern_generalization intern env ntnvars loc bk ak c =
             GLambda (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None), acc))
     in
       List.fold_right (fun ({loc;v=id} as lid) (env, acc) ->
-        let env' = push_name_env ntnvars (Variable,[],[]) env CAst.(make @@ Name id) in
+        let env' = push_name_env ntnvars [] env CAst.(make @@ Name id) in
           (env', abs lid acc)) fvs (env,c)
   in c'
 
@@ -677,7 +677,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam
     if onlyident then
       (* Do not try to interpret a variable as a constructor *)
       let na = out_patvar pat in
-      let env = push_name_env ntnvars (Variable,[],[]) env (make ?loc:pat.loc na) in
+      let env = push_name_env ntnvars [] env (make ?loc:pat.loc na) in
       (renaming,env), None, na
     else
       (* Interpret as a pattern *)
@@ -2084,7 +2084,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
             List.rev_append match_td matchs)
           tms ([],Id.Set.empty,Id.Map.empty,[]) in
         let env' = Id.Set.fold
-          (fun var bli -> push_name_env ntnvars (Variable,[],[]) bli (CAst.make @@ Name var))
+          (fun var bli -> push_name_env ntnvars [] bli (CAst.make @@ Name var))
           (Id.Set.union ex_ids as_in_vars)
           (restart_lambda_binders env)
         in
@@ -2122,17 +2122,17 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
         (* "in" is None so no match to add *)
         let ((b',(na',_)),_,_) = intern_case_item env' Id.Set.empty (b,na,None) in
         let p' = Option.map (fun u ->
-          let env'' = push_name_env ntnvars (Variable,[],[]) env'
+          let env'' = push_name_env ntnvars [] env'
             (CAst.make na') in
           intern_type (slide_binders env'') u) po in
         DAst.make ?loc @@
         GLetTuple (List.map (fun { CAst.v } -> v) nal, (na', p'), b',
-                   intern (List.fold_left (push_name_env ntnvars (Variable,[],[])) env nal) c)
+                   intern (List.fold_left (push_name_env ntnvars []) env nal) c)
     | CIf (c, (na,po), b1, b2) ->
       let env' = reset_tmp_scope env in
       let ((c',(na',_)),_,_) = intern_case_item env' Id.Set.empty (c,na,None) in (* no "in" no match to ad too *)
       let p' = Option.map (fun p ->
-          let env'' = push_name_env ntnvars (Variable,[],[]) env
+          let env'' = push_name_env ntnvars [] env
             (CAst.make na') in
           intern_type (slide_binders env'') p) po in
         DAst.make ?loc @@