Moving the diversity of constr printers to a label style.

This allows to give access to all printing options (e.g. a scope or
being-in-context) to every printer w/o increasing the numbers of
functions.

2 files changed, 19 insertions, 20 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index a31dddbbd5..28f4f5aed6 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1199,7 +1199,15 @@ let extern_glob_type vars c =
 (******************************************************************)
 (* Main translation function from constr -> constr_expr *)
 
-let extern_constr_gen lax goal_concl_style scopt env sigma t =
+let extern_constr ?lax ?(inctx=false) ?scope env sigma t =
+  let r = Detyping.detype Detyping.Later ?lax false Id.Set.empty env sigma t in
+  let vars = vars_of_env env in
+  extern inctx (InConstrEntrySomeLevel,(scope,[])) vars r
+
+let extern_constr_in_scope ?lax ?inctx scope env sigma t =
+  extern_constr ?lax ?inctx ~scope env sigma t
+
+let extern_type ?lax ?(goal_concl_style=false) env sigma t =
   (* "goal_concl_style" means do alpha-conversion using the "goal" convention *)
   (* i.e.: avoid using the names of goal/section/rel variables and the short *)
   (* names of global definitions of current module when computing names for *)
@@ -1208,30 +1216,18 @@ let extern_constr_gen lax goal_concl_style scopt env sigma t =
   (* those goal/section/rel variables that occurs in the subterm under *)
   (* consideration; see namegen.ml for further details *)
   let avoid = if goal_concl_style then vars_of_env env else Id.Set.empty in
-  let r = Detyping.detype Detyping.Later ~lax:lax goal_concl_style avoid env sigma t in
-  let vars = vars_of_env env in
-  extern false (InConstrEntrySomeLevel,(scopt,[])) vars r
-
-let extern_constr_in_scope goal_concl_style scope env sigma t =
-  extern_constr_gen false goal_concl_style (Some scope) env sigma t
-
-let extern_constr ?(lax=false) goal_concl_style env sigma t =
-  extern_constr_gen lax goal_concl_style None env sigma t
-
-let extern_type goal_concl_style env sigma t =
-  let avoid = if goal_concl_style then vars_of_env env else Id.Set.empty in
-  let r = Detyping.detype Detyping.Later goal_concl_style avoid env sigma t in
+  let r = Detyping.detype Detyping.Later ?lax goal_concl_style avoid env sigma t in
   extern_glob_type (vars_of_env env) r
 
 let extern_sort sigma s = extern_glob_sort (detype_sort sigma s)
 
-let extern_closed_glob ?lax goal_concl_style env sigma t =
+let extern_closed_glob ?lax ?(goal_concl_style=false) ?(inctx=false) ?scope env sigma t =
   let avoid = if goal_concl_style then vars_of_env env else Id.Set.empty in
   let r =
     Detyping.detype_closed_glob ?lax goal_concl_style avoid env sigma t
   in
   let vars = vars_of_env env in
-  extern false (InConstrEntrySomeLevel,(None,[])) vars r
+  extern inctx (InConstrEntrySomeLevel,(scope,[])) vars r
 
 (******************************************************************)
 (* Main translation function from pattern -> constr_expr *)
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index aa6aa5f5f9..fa263cbeb7 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -28,7 +28,8 @@ val extern_glob_constr : Id.Set.t -> 'a glob_constr_g -> constr_expr
 val extern_glob_type : Id.Set.t -> 'a glob_constr_g -> constr_expr
 val extern_constr_pattern : names_context -> Evd.evar_map ->
   constr_pattern -> constr_expr
-val extern_closed_glob : ?lax:bool -> bool -> env -> Evd.evar_map -> closed_glob_constr -> constr_expr
+val extern_closed_glob : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool -> ?scope:scope_name ->
+  env -> Evd.evar_map -> closed_glob_constr -> constr_expr
 
 (** If [b=true] in [extern_constr b env c] then the variables in the first
    level of quantification clashing with the variables in [env] are renamed.
@@ -36,10 +37,12 @@ val extern_closed_glob : ?lax:bool -> bool -> env -> Evd.evar_map -> closed_glob
     env, sigma
 *)
 
-val extern_constr : ?lax:bool -> bool -> env -> Evd.evar_map -> constr -> constr_expr
-val extern_constr_in_scope : bool -> scope_name -> env -> Evd.evar_map -> constr -> constr_expr
+val extern_constr : ?lax:bool -> ?inctx:bool -> ?scope:scope_name ->
+  env -> Evd.evar_map -> constr -> constr_expr
+val extern_constr_in_scope : ?lax:bool -> ?inctx:bool -> scope_name ->
+  env -> Evd.evar_map -> constr -> constr_expr
 val extern_reference : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid
-val extern_type : bool -> env -> Evd.evar_map -> types -> constr_expr
+val extern_type : ?lax:bool -> ?goal_concl_style:bool -> env -> Evd.evar_map -> types -> constr_expr
 val extern_sort : Evd.evar_map -> Sorts.t -> glob_sort
 val extern_rel_context : constr option -> env -> Evd.evar_map ->
   rel_context -> local_binder_expr list