From 2e3cf396ba869987c4e41f46bc9b4b2fe31ab4d2 Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 5 Oct 2012 17:59:10 +0000 Subject: Fix a confusion between types of locations in an untyped part of the parser after the migration of compat.ml4 This was leading to huge positions written to .glob files, making coqdoc loop forever. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15861 85f007b7-540e-0410-9357-904b9bb8a0f7 --- parsing/egramcoq.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'parsing') diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 762379803..293520a55 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -65,7 +65,7 @@ let make_constr_action (f : Loc.t -> constr_notation_substitution -> constr_expr) pil = let rec make (constrs,constrlists,binders as fullsubst) = function | [] -> - Gram.action (fun loc -> f loc fullsubst) + Gram.action (fun (loc:CompatLoc.t) -> f (!@loc) fullsubst) | (GramConstrTerminal _ | GramConstrNonTerminal (_,None)) :: tl -> (* parse a non-binding item *) Gram.action (fun _ -> make fullsubst tl) @@ -113,7 +113,10 @@ let make_cases_pattern_action (f : Loc.t -> cases_pattern_notation_substitution -> cases_pattern_expr) pil = let rec make (env,envlist,hasbinders as fullenv) = function | [] -> - Gram.action (fun loc -> f loc (check_cases_pattern_env loc fullenv)) + Gram.action + (fun (loc:CompatLoc.t) -> + let loc = !@loc in + f loc (check_cases_pattern_env loc fullenv)) | (GramConstrTerminal _ | GramConstrNonTerminal (_,None)) :: tl -> (* parse a non-binding item *) Gram.action (fun _ -> make fullenv tl) -- cgit v1.2.3