aboutsummaryrefslogtreecommitdiff
path: root/parsing
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2014-12-16 14:33:43 +0100
committerPierre-Marie Pédrot2014-12-16 14:38:51 +0100
commitf88cce2698da000ab9054da31330db70997a41a4 (patch)
tree8bc74094c06411792ff1431c4ce73c77ec94bb2f /parsing
parent5ba84979df97996cd04f44e506742bb58ecf0465 (diff)
Fixing CAMLP4 compilation.
Diffstat (limited to 'parsing')
-rw-r--r--parsing/compat.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/compat.ml4 b/parsing/compat.ml4
index ce0390e1d2..4c63b95f53 100644
--- a/parsing/compat.ml4
+++ b/parsing/compat.ml4
@@ -221,7 +221,7 @@ end
module GrammarMake (L:LexerSig) : GrammarSig = struct
(* We need to refer to Coq's module Loc before it is hidden by include *)
- let raise_coq_loc loc e = raise (Loc.add_loc e (to_coqloc loc))
+ let raise_coq_loc loc e = Loc.raise (to_coqloc loc) e
include Camlp4.Struct.Grammar.Static.Make (L)
type 'a entry = 'a Entry.t
type action = Action.t