[ defs = LIST1 [
name = IDENT;
args = LIST1 [
- PAREN "(" ; names = LIST1 IDENT SEP SYMBOL ","; SYMBOL ":";
- ty = term; PAREN ")" ->
- (names, ty)
+ PAREN "(" ; names = LIST1 IDENT SEP SYMBOL ",";
+ SYMBOL ":"; ty = term; PAREN ")" ->
+ (names, Some ty)
+ | name = IDENT -> [name],None
];
index_name = OPT [ IDENT "on"; idx = IDENT -> idx ];
ty = OPT [ SYMBOL ":" ; t = term -> t ];
list_of_binder binder ty
(binder_of_arg_list binder final_term tl) l
in
+ let args =
+ List.map
+ (function
+ names,Some ty -> names,ty
+ | names,None -> names,CicAst.Implicit
+ ) args in
let t1' = binder_of_arg_list `Lambda t1 args in
let ty' =
match ty with
return_term loc (CicAst.Meta (index, substs))
| outtyp = OPT [ PAREN "["; typ = term; PAREN "]" -> typ ];
"match"; t = term;
- indty_ident = OPT [ SYMBOL ":"; id = IDENT -> id ];
+ indty_ident = OPT ["in" ; id = IDENT -> id ];
"with";
PAREN "[";
patterns = LIST0 [
| [ IDENT "intro" ] ->
TacticAst.Intros (loc, Some 1, [])
| [ IDENT "left" ] -> TacticAst.Left loc
- | [ "let" | "Let" ];
- t = tactic_term; "in"; where = IDENT ->
+ | [ IDENT "letin" ];
+ where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
TacticAst.LetIn (loc, t, where)
| kind = reduction_kind;
pat = OPT [
let name,ty =
match defs with
| ((Cic.Name name,Some ty),_,_) :: _ -> name,ty
- | ((Cic.Name name,None),_,_) :: _ ->
- fail loc ("No type given for " ^ name)
+ | ((Cic.Name name,None),_,_) :: _ -> name,CicAst.Implicit
| _ -> assert false
in
let body = CicAst.Ident (name,None) in