diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-29 23:36:32 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-29 23:36:32 +0000 |
| commit | 7264f8df4300014b945294fc21cecb1c4ad07513 (patch) | |
| tree | 2e887caaf4eda96d813e15c9d37635f01ea0f934 /parsing/egrammar.ml | |
| parent | f4ac1e7eca690e0184da9096942b510ccf0991b1 (diff) | |
Utilisation de Snext pour gérer les symboles non associatifs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3343 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/egrammar.ml')
| -rw-r--r-- | parsing/egrammar.ml | 11 |
1 files changed, 1 insertions, 10 deletions
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index 42a23b4c8..ade148afe 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -45,11 +45,6 @@ let constr_level = function | 8,assoc -> assert (assoc <> Gramext.LeftA); "top" | n,assoc -> (string_of_int n)^(assoc_level assoc) -let constr_prod_level = function - | 8 -> "top" - | 4 -> "4L" - | n -> string_of_int n - let default_levels = [8,Gramext.RightA; 1,Gramext.RightA; 0,Gramext.RightA] let level_stack = ref [default_levels] @@ -191,11 +186,7 @@ let rec build_prod_item univ assoc = function | ProdList0 s -> Gramext.Slist0 (build_prod_item univ assoc s) | ProdList1 s -> Gramext.Slist1 (build_prod_item univ assoc s) | ProdOpt s -> Gramext.Sopt (build_prod_item univ assoc s) - | ProdPrimitive typ -> - match get_constr_production_entry assoc typ with - | (eobj,None) -> Gramext.Snterm (Gram.Entry.obj eobj) - | (eobj,Some lev) -> - Gramext.Snterml (Gram.Entry.obj eobj,constr_prod_level lev) + | ProdPrimitive typ -> symbol_of_production assoc typ let symbol_of_prod_item univ assoc = function | Term tok -> (Gramext.Stoken tok, None) |