From ab7fd497575b161eeb9bfe89da743b3fbc93aaf3 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 15 Nov 2017 21:44:32 +0100 Subject: Fixing factorization of recursive notations in the case of an atomic separator. This addresses a limitation found in math-comp seq.v file. See the example in test suite file success/Notations2.v. To go further and accept recursive notations with a separator made of several tokens, and assuming camlp5 unchanged, one would need to declare an auxiliary entry for this sequence of tokens and use it as an "atomic" (non-terminal) separator. See PR #6167 for details. --- parsing/egramcoq.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'parsing') diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index d51b8b54e..9504768a8 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -259,9 +259,11 @@ let is_binder_level from e = match e with | (NumLevel 200, (BorderProd (Right, _) | InternalProd)) -> from = 200 | _ -> false -let make_sep_rules tkl = - let rec mkrule : Tok.t list -> unit rules = function - | [] -> Rules ({ norec_rule = Stop }, ignore) +let make_sep_rules = function + | [tk] -> Atoken tk + | tkl -> + let rec mkrule : Tok.t list -> string rules = function + | [] -> Rules ({ norec_rule = Stop }, fun _ -> (* dropped anyway: *) "") | tkn :: rem -> let Rules ({ norec_rule = r }, f) = mkrule rem in let r = { norec_rule = Next (r, Atoken tkn) } in -- cgit v1.2.3