From 8b78dec71c7922ab335a554d28b320423efbb9d3 Mon Sep 17 00:00:00 2001 From: glondu Date: Tue, 28 Sep 2010 15:32:17 +0000 Subject: Remove some occurrences of "open Termops" Functions from Termops were sometimes fully qualified, sometimes not in the same module. This commit makes their usage more uniform. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13470 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/rtauto/refl_tauto.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'plugins/rtauto/refl_tauto.ml') 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 -- cgit v1.2.3