From 17c5ad881e737bd2cba2e157f346a618fce87204 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 26 May 2005 14:13:23 +0000 Subject: [PATCH] fixed issue with explicit named substitutions --- .../cic_disambiguation/cicTextualParser2.ml | 20 +++++++++---------- 1 file changed, 9 insertions(+), 11 deletions(-) diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index add74d03e..bfc535a3c 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -147,20 +147,18 @@ EXTEND ] ]; subst: [ - [ subst = OPT [ - SYMBOL "\\subst"; (* to avoid catching frequent "a [1]" cases *) - PAREN "["; - substs = LIST1 [ - i = IDENT; SYMBOL <:unicode> (* ≔ *); t = term -> (i, t) - ] SEP SYMBOL ";"; - PAREN "]" -> - substs - ] -> subst + [ SYMBOL "\\subst"; (* to avoid catching frequent "a [1]" cases *) + PAREN "["; + substs = LIST1 [ + i = IDENT; SYMBOL <:unicode> (* ≔ *); t = term -> (i, t) + ] SEP SYMBOL ";"; + PAREN "]" -> + substs ] ]; substituted_name: [ (* a subs.name is an explicit substitution subject *) - [ s = IDENT; subst = subst -> CicAst.Ident (s, subst) - | s = URI; subst = subst -> CicAst.Uri (ind_expansion s, subst) + [ s = IDENT; subst = OPT subst -> CicAst.Ident (s, subst) + | s = URI; subst = OPT subst -> CicAst.Uri (ind_expansion s, subst) ] ]; name: [ (* as substituted_name with no explicit substitution *) -- 2.39.2