aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind/glob_termops.mli
diff options
context:
space:
mode:
authorGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-06-22 15:14:30 +0000
committerGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-06-22 15:14:30 +0000
commit6b45f2d36929162cf92272bb60c2c245d9a0ead3 (patch)
tree93aa975697b7de73563c84773d99b4c65b92173b /plugins/funind/glob_termops.mli
parentfea214f82954197d23fda9a0e4e7d93e0cbf9b4c (diff)
Added an indirection with respect to Loc in Compat. As many [open Compat]
were closed (i.e. the only remaining ones are those of printing/parsing). Meanwhile, a simplified interface is provided in loc.mli. This also permits to put Pp in Clib, because it does not depend on CAMLP4/5 anymore. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15475 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/funind/glob_termops.mli')
-rw-r--r--plugins/funind/glob_termops.mli6
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli
index 437ba225d..9cf83df15 100644
--- a/plugins/funind/glob_termops.mli
+++ b/plugins/funind/glob_termops.mli
@@ -15,7 +15,7 @@ val pattern_to_term : cases_pattern -> glob_constr
(*
Some basic functions to rebuild glob_constr
- In each of them the location is Util.dummy_loc
+ In each of them the location is Util.Loc.ghost
*)
val mkGRef : Globnames.global_reference -> glob_constr
val mkGVar : Names.identifier -> glob_constr
@@ -85,9 +85,9 @@ val alpha_rt : Names.identifier list -> glob_constr -> glob_constr
(* same as alpha_rt but for case branches *)
val alpha_br : Names.identifier list ->
- Pp.loc * Names.identifier list * Glob_term.cases_pattern list *
+ Loc.t * Names.identifier list * Glob_term.cases_pattern list *
Glob_term.glob_constr ->
- Pp.loc * Names.identifier list * Glob_term.cases_pattern list *
+ Loc.t * Names.identifier list * Glob_term.cases_pattern list *
Glob_term.glob_constr