diff options
| author | Hugo Herbelin | 2020-05-13 17:06:44 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-05-13 17:22:05 +0200 |
| commit | 8f5e1e166e7e174ff393a2a8fa2b11188745b19e (patch) | |
| tree | 7ce7c8c8b3155a8708211f13d555ac2c09e53945 /plugins | |
| parent | 1e80f730590ba309b6eb1ae26832984fa7357761 (diff) | |
Ssrmatching: Hack to circumvent a hack.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index adaf7c8cc1..ce6fd4939b 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -370,6 +370,11 @@ let ehole_var = EConstr.mkVar (Id.of_string "_") let pr_econstr_pat env sigma c0 = let rec wipe_evar c = let open EConstr in if isEvar sigma c then ehole_var else map sigma wipe_evar c in + let dummy_decl = + let dummy_prod = mkProd (make_annot Anonymous Sorts.Relevant,mkProp,mkProp) in + let na = make_annot (EConstr.destVar sigma ehole_var) Sorts.Relevant in + Context.Named.Declaration.(LocalAssum (na, dummy_prod)) in + let env = Environ.push_named dummy_decl env in pr_econstr_env env sigma (wipe_evar c0) (* Turn (new) evars into metas *) |