From 2546d722c98810ab6369b72c2f384d02d74afb26 Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 4 Nov 2003 21:24:53 +0000 Subject: En v8, une notation, c'est 2 regles et un niveau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4795 85f007b7-540e-0410-9357-904b9bb8a0f7 --- parsing/egrammar.ml | 19 +++++++++++-------- 1 file changed, 11 insertions(+), 8 deletions(-) diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index e82fd8025..ef41a0283 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -411,23 +411,26 @@ let factorize_grams l1 l2 = let number_of_entries gcl = List.fold_left - (fun n -> function - | Notation _ -> n + 1 - | Grammar gc -> n + (List.length gc.gc_entries) - | TacticGrammar l -> n + 1) - 0 gcl + (fun (n,l) -> function + | Notation _ -> + (if !Options.v7 then n + 1 + else n + 2 (* 1 for operconstr, 1 for pattern *)), l + 1 + | Grammar gc -> + n + (List.length gc.gc_entries), l + (List.length gc.gc_entries) + | TacticGrammar _ -> n + 1, l + 1) + (0,0) gcl let unfreeze (grams, lex) = let (undo, redo, common) = factorize_grams !grammar_state grams in - let n = number_of_entries undo in + let n,l = number_of_entries undo in remove_grammars n; - remove_levels n; + remove_levels l; grammar_state := common; Lexer.unfreeze lex; List.iter extend_grammar (List.rev redo) let init_grammar () = - remove_grammars (number_of_entries !grammar_state); + remove_grammars (fst (number_of_entries !grammar_state)); grammar_state := [] let init () = -- cgit v1.2.3