From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 26 May 2005 14:13:23 +0000 (+0000)
Subject: fixed issue with explicit named substitutions
X-Git-Tag: PRE_INDEX_1~119
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=17c5ad881e737bd2cba2e157f346a618fce87204;p=helm.git

fixed issue with explicit named substitutions
---

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<Assign>> (* ≔ *); 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<Assign>> (* ≔ *); 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 *)