diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-04 14:48:36 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:23:49 +0100 |
| commit | d528fdaf12b74419c47698cca7c6f1ec762245a3 (patch) | |
| tree | 2edbaac4e19db595e0ec763de820cbc704897043 /plugins/rtauto | |
| parent | 6bd193ff409b01948751525ce0f905916d7a64bd (diff) | |
Retyping API using EConstr.
Diffstat (limited to 'plugins/rtauto')
| -rw-r--r-- | plugins/rtauto/refl_tauto.ml | 8 |
1 files changed, 4 insertions, 4 deletions
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 |