diff options
| author | Pierre-Marie Pédrot | 2020-10-15 15:15:44 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-10-15 15:15:44 +0200 |
| commit | 476520ab32d3e975f6cee8aabcd04ad5fdfbbd77 (patch) | |
| tree | e8a75d0411c275635540f675449cc38b00c989fd /plugins/ssr | |
| parent | 4bf43453ec5f635ae87a2edeb4f51d95f2d5ac67 (diff) | |
| parent | 92ddd42345f9976a1e3b2cc2e53541ef0864ed0b (diff) | |
Merge PR #13098: Deprecating wit_var to the benefit of its synonymous wit_hyp
Reviewed-by: ejgallego
Reviewed-by: gares
Ack-by: jfehrle
Reviewed-by: ppedrot
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrparser.mlg | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index d859fe51ab..cb58b9bcb8 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -280,7 +280,7 @@ let interp_wit wit ist gl x = sigma, Tacinterp.Value.cast (topwit wit) arg let interp_hyp ist gl (SsrHyp (loc, id)) = - let s, id' = interp_wit wit_var ist gl CAst.(make ?loc id) in + let s, id' = interp_wit wit_hyp ist gl CAst.(make ?loc id) in if not_section_id id' then s, SsrHyp (loc, id') else hyp_err ?loc "Can't clear section hypothesis " id' diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 89e0c9fcbe..7b584b5159 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -155,7 +155,7 @@ let pr_ssrhyp _ _ _ = pr_hyp let wit_ssrhyprep = add_genarg "ssrhyprep" (fun env sigma -> pr_hyp) let intern_hyp ist (SsrHyp (loc, id) as hyp) = - let _ = Tacintern.intern_genarg ist (in_gen (rawwit wit_var) CAst.(make ?loc id)) in + let _ = Tacintern.intern_genarg ist (in_gen (rawwit wit_hyp) CAst.(make ?loc id)) in if not_section_id id then hyp else hyp_err ?loc "Can't clear section hypothesis " id |