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
[
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 ->
| "whd" -> `Whd ]
];
tactic: [
- [ [ IDENT "absurd" | IDENT "Absurd" ] -> return_tactic loc TacticAst.Absurd
- | [ IDENT "apply" | IDENT "Apply" ];
- t = tactic_term -> return_tactic loc (TacticAst.Apply t)
+ [ [ IDENT "absurd" | IDENT "Absurd" ]; t = tactic_term ->
+ return_tactic loc (TacticAst.Absurd t)
+ | [ IDENT "apply" | IDENT "Apply" ]; t = tactic_term ->
+ return_tactic loc (TacticAst.Apply t)
| [ IDENT "assumption" | IDENT "Assumption" ] ->
return_tactic loc TacticAst.Assumption
| [ IDENT "change" | IDENT "Change" ];
| [ IDENT "discriminate" | IDENT "Discriminate" ];
hyp = IDENT ->
return_tactic loc (TacticAst.Discriminate hyp)
- | [ IDENT "elim" | IDENT "Elim" ]; IDENT "type";
- t = tactic_term ->
+ | [ IDENT "elimType" | IDENT "ElimType" ]; t = tactic_term ->
return_tactic loc (TacticAst.ElimType t)
| [ IDENT "elim" | IDENT "Elim" ];
t1 = tactic_term;
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" ];
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) ]
return_command loc (TacticAst.Undo (int_opt steps))
| [ IDENT "redo" | IDENT "Redo" ]; steps = OPT NUM ->
return_command loc (TacticAst.Redo (int_opt steps))
+ | [ IDENT "check" | IDENT "Check" ]; t = term ->
+ return_command loc (TacticAst.Check t)
]
];
END