diff options
| author | Pierre Corbineau | 2014-12-16 15:59:52 +0100 |
|---|---|---|
| committer | Pierre Corbineau | 2014-12-16 16:01:25 +0100 |
| commit | 8029f7555f9c6f201cc70b5ecc538b11a861f0aa (patch) | |
| tree | c750b3ea7cafd5ec2176866bbd16208e5335978a /parsing | |
| parent | d4f5bdd6f7304fac541bb5f4555ecdd6aa42699a (diff) | |
| parent | f88cce2698da000ab9054da31330db70997a41a4 (diff) | |
fix bug #2447 in congruence
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/compat.ml4 | 4 | ||||
| -rw-r--r-- | parsing/egramcoq.ml | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/parsing/compat.ml4 b/parsing/compat.ml4 index f872c4a2d8..4c63b95f53 100644 --- a/parsing/compat.ml4 +++ b/parsing/compat.ml4 @@ -193,7 +193,7 @@ module GrammarMake (L:LexerSig) : GrammarSig = struct let entry_create = Entry.create let entry_parse e p = try Entry.parse e p - with Exc_located (loc,e) -> raise (Loc.add_loc e (to_coqloc loc)) + with Exc_located (loc,e) -> Loc.raise (to_coqloc loc) e IFDEF CAMLP5_6_02_1 THEN let entry_print ft x = Entry.print ft x ELSE @@ -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 diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index a0384faf84..9f49638618 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -355,7 +355,7 @@ let with_grammar_rule_protection f x = with reraise -> let reraise = Errors.push reraise in let () = unfreeze fs in - raise reraise + iraise reraise (**********************************************************************) (** Ltac quotations *) |