diff options
| author | coqbot-app[bot] | 2020-11-06 11:48:52 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-06 11:48:52 +0000 |
| commit | e5dc6e5cd189fb0e6fff672d7e978c62b4d4c160 (patch) | |
| tree | 39a95b8536b9523ee1c11ce87a373d5cc625752b /interp | |
| parent | d7bf4b407052ca71f4e642d932606ba9e7ac49ee (diff) | |
| parent | 3515988d1b9f792bf6f4e921f4776c5fe574b3ed (diff) | |
Merge PR #13255: Fixes #13244: support for coercions in Search
Reviewed-by: SkySkimmer
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 8 | ||||
| -rw-r--r-- | interp/constrintern.mli | 6 |
2 files changed, 14 insertions, 0 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 409e46864e..ecf2b951a2 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -2518,6 +2518,14 @@ let intern_constr_pattern env sigma ?(as_type=false) ?(ltacvars=empty_ltac_sign) ~pattern_mode:true ~ltacvars env sigma c in pattern_of_glob_constr c +let interp_constr_pattern env sigma ?(expected_type=WithoutTypeConstraint) c = + let c = intern_gen expected_type ~pattern_mode:true env sigma c in + let flags = { Pretyping.no_classes_no_fail_inference_flags with expand_evars = false } in + let sigma, c = understand_tcc ~flags env sigma ~expected_type c in + (* FIXME: it is necessary to be unsafe here because of the way we handle + evars in the pretyper. Sometimes they get solved eagerly. *) + pattern_of_constr env sigma (EConstr.Unsafe.to_constr c) + let intern_core kind env sigma ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign) { Genintern.intern_ids = ids; Genintern.notation_variable_status = vl } c = let tmp_scope = scope_of_type_kind env sigma kind in 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 |