fixed issue with explicit named substitutions

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index add74d03e856cde6162bf7064d66f3ec6da489c9..bfc535a3c35f59b204ccd8d7706d7df3fb15d8af 100644 (file)
--- 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 *)