diff options
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 30 |
1 files changed, 13 insertions, 17 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index a31dddbbd5..cc0c1e4602 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -678,7 +678,7 @@ let remove_one_coercion inctx c = try match match_coercion_app c with | Some (loc,r,pars,args) when not (!Flags.raw_print || !print_coercions) -> let nargs = List.length args in - (match Classops.hide_coercion r with + (match Coercionops.hide_coercion r with | Some n when (n - pars) < nargs && (inctx || (n - pars)+1 < nargs) -> (* We skip the coercion *) let l = List.skipn (n - pars) args in @@ -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 *) |