diff options
| author | Hugo Herbelin | 2020-10-22 19:41:15 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-04 17:49:21 +0100 |
| commit | 011de69dab3afcd265f6e38aab05548654a606c8 (patch) | |
| tree | f45cf801544b7dc4a5fc186a2d1610369bcb9edd /interp/constrintern.mli | |
| parent | 7f90e6e0aa8dd27c64bac0dbc4b247ebb33d4aca (diff) | |
Adding a typed interpretation of patterns.
Diffstat (limited to 'interp/constrintern.mli')
| -rw-r--r-- | interp/constrintern.mli | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 898a3e09c8..11d756803f 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -136,10 +136,16 @@ val interp_type_evars_impls : ?flags:inference_flags -> env -> evar_map -> (** Interprets constr patterns *) +(** Without typing *) val intern_constr_pattern : env -> evar_map -> ?as_type:bool -> ?ltacvars:ltac_sign -> constr_pattern_expr -> patvar list * constr_pattern +(** With typing *) +val interp_constr_pattern : + env -> evar_map -> ?expected_type:typing_constraint -> + constr_pattern_expr -> constr_pattern + (** Raise Not_found if syndef not bound to a name and error if unexisting ref *) val intern_reference : qualid -> GlobRef.t |