diff options
Diffstat (limited to 'interp/constrintern.mli')
| -rw-r--r-- | interp/constrintern.mli | 16 |
1 files changed, 11 insertions, 5 deletions
diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 2b87d0d66d..91a3454766 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -33,11 +33,13 @@ open Termops - insert existential variables for implicit arguments *) -type implicits_env = (* To interpret inductive type with implicits *) - (identifier * (identifier list * Impargs.implicits_list)) list +(* To interpret implicits and arg scopes of recursive variables in + inductive types and recursive definitions *) +type var_internalisation_data = + identifier list * Impargs.implicits_list * scope_name option list -type full_implicits_env = - identifier list * implicits_env +type implicits_env = (identifier * var_internalisation_data) list +type full_implicits_env = identifier list * implicits_env type ltac_sign = identifier list * (identifier * identifier option) list @@ -66,8 +68,12 @@ val interp_casted_openconstr : val interp_type_with_implicits : evar_map -> env -> full_implicits_env -> constr_expr -> types +val interp_casted_constr_with_implicits : + evar_map -> env -> implicits_env -> constr_expr -> types -> constr + val interp_rawconstr_with_implicits : - env -> identifier list -> implicits_env -> constr_expr -> rawconstr + evar_map -> env -> identifier list -> implicits_env -> constr_expr -> + rawconstr (*s Build a judgement from *) val judgment_of_rawconstr : evar_map -> env -> constr_expr -> unsafe_judgment |