diff options
Diffstat (limited to 'interp/constrintern.mli')
| -rw-r--r-- | interp/constrintern.mli | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/interp/constrintern.mli b/interp/constrintern.mli index c052dadabf..4f0c803bdc 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -44,7 +44,7 @@ type ltac_env = (* Interprets global names, including syntactic defs and section variables *) val interp_rawconstr : evar_map -> env -> constr_expr -> rawconstr val interp_rawconstr_gen : bool -> evar_map -> env -> implicits_env -> - patvar list option -> ltac_sign -> constr_expr -> rawconstr + bool -> ltac_sign -> constr_expr -> rawconstr (*s Composing the translation with typing *) val interp_constr : evar_map -> env -> constr_expr -> constr @@ -70,14 +70,13 @@ val type_judgment_of_rawconstr : (* Interprets a constr according to two lists of instantiations (variables and metas), possibly casting it*) val interp_constr_gen : - evar_map -> env -> ltac_env -> patvar_map -> constr_expr -> - constr option -> constr + evar_map -> env -> ltac_env -> constr_expr -> constr option -> constr (* Interprets a constr according to two lists of instantiations (variables and metas), possibly casting it, and turning unresolved evar into metas*) val interp_openconstr_gen : evar_map -> env -> ltac_env -> - patvar_map -> constr_expr -> constr option -> evar_map * constr + constr_expr -> constr option -> evar_map * constr (* Interprets constr patterns according to a list of instantiations (variables)*) |