diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-10-05 17:59:10 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-10-05 17:59:10 +0000 |
| commit | 2e3cf396ba869987c4e41f46bc9b4b2fe31ab4d2 (patch) | |
| tree | 4da162a9a1c2c937f4e12524b13f7f0b76dcb13c /parsing | |
| parent | 87b9f636f602e6067314ac994777e54307a72a65 (diff) | |
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
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/egramcoq.ml | 7 |
1 files changed, 5 insertions, 2 deletions
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) |