From d528fdaf12b74419c47698cca7c6f1ec762245a3 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 4 Nov 2016 14:48:36 +0100 Subject: Retyping API using EConstr. --- plugins/rtauto/refl_tauto.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'plugins/rtauto') diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index b129b0bb3..f88b3a700 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -94,9 +94,9 @@ let rec make_form atom_env gls term = let cciterm=special_whd gls term in match kind_of_term cciterm with Prod(_,a,b) -> - if EConstr.Vars.noccurn Evd.empty (** FIXME *) 1 (EConstr.of_constr b) && + if EConstr.Vars.noccurn (Tacmach.project gls) 1 (EConstr.of_constr b) && Retyping.get_sort_family_of - (pf_env gls) (Tacmach.project gls) a == InProp + (pf_env gls) (Tacmach.project gls) (EConstr.of_constr a) == InProp then let fa=make_form atom_env gls a in let fb=make_form atom_env gls b in @@ -136,7 +136,7 @@ let rec make_hyps atom_env gls lenv = function make_hyps atom_env gls (typ::lenv) rest in if List.exists (fun c -> Termops.local_occur_var Evd.empty (** FIXME *) id (EConstr.of_constr c)) lenv || (Retyping.get_sort_family_of - (pf_env gls) (Tacmach.project gls) typ != InProp) + (pf_env gls) (Tacmach.project gls) (EConstr.of_constr typ) != InProp) then hrec else @@ -262,7 +262,7 @@ let rtauto_tac gls= let gl=pf_concl gls in let _= if Retyping.get_sort_family_of - (pf_env gls) (Tacmach.project gls) gl != InProp + (pf_env gls) (Tacmach.project gls) (EConstr.of_constr gl) != InProp then user_err ~hdr:"rtauto" (Pp.str "goal should be in Prop") in let glf=make_form gamma gls gl in let hyps=make_hyps gamma gls [gl] (pf_hyps gls) in -- cgit v1.2.3