From bf4112094feb1a705d8bdaea3fb0febc4ef3ff59 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 24 Oct 2017 14:35:25 +0200 Subject: [general] Remove Econstr dependency from `intf` To this extent we factor out the relevant bits to a new file, ltac_pretype. --- plugins/ssr/ssrcommon.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/ssr') diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index d37c676e3..1f2d02093 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -227,7 +227,7 @@ let isAppInd gl c = let interp_refine ist gl rc = let constrvars = Tacinterp.extract_ltac_constr_values ist (pf_env gl) in let vars = { Glob_ops.empty_lvar with - Glob_term.ltac_constrs = constrvars; ltac_genargs = ist.Tacinterp.lfun + Ltac_pretype.ltac_constrs = constrvars; ltac_genargs = ist.Tacinterp.lfun } in let kind = Pretyping.OfType (pf_concl gl) in let flags = { -- cgit v1.2.3