diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-09-28 15:32:17 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-09-28 15:32:17 +0000 |
| commit | 8b78dec71c7922ab335a554d28b320423efbb9d3 (patch) | |
| tree | d8cd3e6744cd3e99a608c53baa0ba04b6288922c /parsing/pptactic.ml | |
| parent | 5754edd0bfc8c38cee2e721ef8d2130c97664f05 (diff) | |
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
Diffstat (limited to 'parsing/pptactic.ml')
| -rw-r--r-- | parsing/pptactic.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 64b8b7bc9..6f0896cc8 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -19,7 +19,6 @@ open Pattern open Ppextend open Ppconstr open Printer -open Termops let pr_global x = Nametab.pr_global_env Idset.empty x @@ -388,11 +387,11 @@ let pr_by_tactic prt = function | tac -> spc() ++ str "by " ++ prt tac let pr_hyp_location pr_id = function - | occs, InHyp -> spc () ++ pr_with_occurrences pr_id occs - | occs, InHypTypeOnly -> + | occs, Termops.InHyp -> spc () ++ pr_with_occurrences pr_id occs + | occs, Termops.InHypTypeOnly -> spc () ++ pr_with_occurrences (fun id -> str "(type of " ++ pr_id id ++ str ")") occs - | occs, InHypValueOnly -> + | occs, Termops.InHypValueOnly -> spc () ++ pr_with_occurrences (fun id -> str "(value of " ++ pr_id id ++ str ")") occs |