From 1e61e4290c96600e3758b30b660712514ba379e3 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 22 Oct 2004 09:54:49 +0000 Subject: [PATCH] - 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 --- .../ocaml/cic_disambiguation/cicTextualParser2.ml | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index 634e8e291..0c00d8698 100644 --- 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) ] -- 2.39.2