aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/pcoq.mli
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-09-15 10:42:13 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-09-15 10:42:13 +0200
commit9e6b192adcaadcdb1935a68f39ce5ea877562188 (patch)
treec0b66a5665b1068c694466e8c64ec57c748530fb /parsing/pcoq.mli
parentd6d7a12eb49c997dd83298477e216349fad74c7f (diff)
parent7f816f00fed5ee7c7e94bd5f02a88880cdfa96aa (diff)
Merge PR #1051: Using an algebraic type for distinguishing toplevel input from location in file
Diffstat (limited to 'parsing/pcoq.mli')
-rw-r--r--parsing/pcoq.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 897e42c30..4e6bff20a 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -73,7 +73,7 @@ module type S =
type coq_parsable
- val parsable : ?file:string -> char Stream.t -> coq_parsable
+ val parsable : ?file:Loc.source -> char Stream.t -> coq_parsable
val action : 'a -> action
val entry_create : string -> 'a entry
val entry_parse : 'a entry -> coq_parsable -> 'a