diff options
Diffstat (limited to 'plugins/rtauto/refl_tauto.ml')
| -rw-r--r-- | plugins/rtauto/refl_tauto.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 3e9cc781f..cd4a7d3b0 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -10,7 +10,6 @@ module Search = Explore.Make(Proof_search) open Util open Term -open Termops open Names open Evd open Tacmach @@ -102,7 +101,7 @@ 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 not (dependent (mkRel 1) b) && + if not (Termops.dependent (mkRel 1) b) && Retyping.get_sort_family_of (pf_env gls) (Tacmach.project gls) a = InProp then @@ -142,7 +141,7 @@ let rec make_hyps atom_env gls lenv = function | (id,None,typ)::rest -> let hrec= make_hyps atom_env gls (typ::lenv) rest in - if List.exists (dependent (mkVar id)) lenv || + if List.exists (Termops.dependent (mkVar id)) lenv || (Retyping.get_sort_family_of (pf_env gls) (Tacmach.project gls) typ <> InProp) then |