- use CicUtil.term_of_uri instead of deprecated HelmLibrayObjects

  similar function
- reverted to old syntax for binders (e.g. \forall x,y:nat.x=y)
- use ";;" as phrases terminator

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 634e8e291bcd2f38871290ac657f180588fd5e89..0c00d869809435ce403d5ce4e5c0130237bc2406 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -47,9 +47,9 @@ let fresh_num_instance =
   else
     (fun () -> 0)
 
-let choice_of_uri (uri: string) =
-  let cic = HelmLibraryObjects.term_of_uri (UriManager.uri_of_string uri) in
-  (uri, (fun _ _ _ -> cic))
+let choice_of_uri uri =
+  let term = CicUtil.term_of_uri uri in
+  (uri, (fun _ _ _ -> term))
 
 let grammar = Grammar.gcreate CicTextualLexer2.cic_lexer
 
@@ -158,12 +158,12 @@ EXTEND
       [
         b = binder;
         (vars, typ) =
-          [ vars = LIST1 IDENT;
+          [ vars = LIST1 IDENT SEP SYMBOL ",";
             typ = OPT [ SYMBOL ":"; t = term -> t ] -> (vars, typ)
-          | PAREN "("; vars = LIST1 IDENT;
+          | PAREN "("; vars = LIST1 IDENT SEP SYMBOL ",";
             typ = OPT [ SYMBOL ":"; t = term -> t ]; PAREN ")" -> (vars, typ)
           ];
-        SYMBOL ","; body = term ->
+        SYMBOL "."; body = term ->
           let binder =
             List.fold_right
               (fun var body ->
@@ -281,6 +281,7 @@ EXTEND
         return_tactic loc (TacticAst.Fold (kind, t))
     | [ IDENT "fourier" | IDENT "Fourier" ] ->
         return_tactic loc TacticAst.Fourier
+    | [ IDENT "hint" | IDENT "Hint" ] -> return_tactic loc TacticAst.Hint
     | [ IDENT "injection" | IDENT "Injection" ]; ident = IDENT ->
         return_tactic loc (TacticAst.Injection ident)
     | [ IDENT "intros" | IDENT "Intros" ];
@@ -312,7 +313,7 @@ EXTEND
         return_tactic loc (TacticAst.Transitivity t)
     ]
   ];
-  tactical0: [ [ t = tactical; SYMBOL "." -> t ] ];
+  tactical0: [ [ t = tactical; SYMBOL ";;" -> t ] ];
   tactical:
     [ "command" NONA
       [ cmd = command -> return_tactical loc (TacticAst.Command cmd) ]