handle Cic.Anonymous

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index d60e563786b29dce42d2edc10a545dcab87cb1a0..0ac8ab38072ec67a81e5567412ebafc5604d2180 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -86,7 +86,8 @@ EXTEND
   term:
     [ "arrow" RIGHTA
       [ t1 = term; SYMBOL <:unicode<to>>; t2 = term ->
-          return_term loc (CicTextualParser2Ast.Binder (`Pi, Cic.Anonymous, Some t1, t2))
+          return_term loc
+            (CicTextualParser2Ast.Binder (`Pi, Cic.Anonymous, Some t1, t2))
       ]
     | "eq" LEFTA
       [ t1 = term; SYMBOL "="; t2 = term ->
@@ -97,13 +98,18 @@ EXTEND
     | "inv" NONA      [ (* nothing here by default *) ]
     | "simple" NONA
       [
-        (* TODO handle "_" *)
         b = binder; vars = LIST1 IDENT SEP SYMBOL ",";
         typ = OPT [ SYMBOL ":"; t = term -> t ];
         SYMBOL "."; body = term ->
           let binder =
             List.fold_right
-              (fun var body -> CicTextualParser2Ast.Binder (b, Cic.Name var, typ, body))
+              (fun var body ->
+                let name =
+                  match var with
+                  | "_" -> Cic.Anonymous
+                  | var -> Cic.Name var
+                in
+                CicTextualParser2Ast.Binder (b, name, typ, body))
               vars body
           in
           return_term loc binder
@@ -115,7 +121,6 @@ EXTEND
       | LPAREN "("; head = term; args = LIST1 term; RPAREN ")" ->
           return_term loc (CicTextualParser2Ast.Appl (head :: args))
       | i = NUM -> return_term loc (CicTextualParser2Ast.Num (i, 0))
-(*       | i = NUM -> return_term loc (CicTextualParser2Ast.Num (i, Random.int max_int)) *)
       | m = META;
         substs = [
           LPAREN "["; substs = LIST0 meta_subst SEP SYMBOL ";" ; RPAREN "]" ->