diff options
| author | Maxime Dénès | 2017-06-14 17:57:28 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-14 17:57:28 +0200 |
| commit | d7dc4d4082d76e480b6d9932dcfad64249565e80 (patch) | |
| tree | 47c24efb25606259c3e0d9c2ac4da2160880a47e /plugins/ssr | |
| parent | 510879170dae6edb989c76a96ded0ed00f192173 (diff) | |
| parent | f713e6c195d1de177b43cab7c2902f5160f6af9f (diff) | |
Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index d389f70859..490ded9d4d 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -226,8 +226,8 @@ let isAppInd gl c = let interp_refine ist gl rc = let constrvars = Tacinterp.extract_ltac_constr_values ist (pf_env gl) in - let vars = { Pretyping.empty_lvar with - Pretyping.ltac_constrs = constrvars; ltac_genargs = ist.Tacinterp.lfun + let vars = { Glob_ops.empty_lvar with + Glob_term.ltac_constrs = constrvars; ltac_genargs = ist.Tacinterp.lfun } in let kind = Pretyping.OfType (pf_concl gl) in let flags = { |