[ 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
| n = substituted_name -> return_term loc n
| i = NUM -> return_term loc (CicAst.Num (i, (fresh_num_instance ())))
| IMPLICIT -> return_term loc CicAst.Implicit
+ | PLACEHOLDER -> return_term loc CicAst.UserInput
| m = META;
substs = [
PAREN "["; substs = LIST0 meta_subst SEP SYMBOL ";" ; PAREN "]" ->
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 [
reduction_kind: [
[ [ IDENT "reduce" ] -> `Reduce
| [ IDENT "simplify" ] -> `Simpl
- | [ IDENT "whd" ] -> `Whd ]
+ | [ IDENT "whd" ] -> `Whd
+ | [ IDENT "normalize" ] -> `Normalize ]
];
tactic: [
[ [ IDENT "absurd" ]; t = tactic_term ->
let idents = match idents with None -> [] | Some idents -> idents in
TacticAst.Intros (loc, num, idents)
| [ IDENT "intro" ] ->
- TacticAst.Intros (loc, None, [])
+ 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 [
| None, terms -> TacticAst.Reduce (loc, kind, Some (terms, `Goal))
| Some pat, [] -> fail loc "Missing term [list]"
| Some pat, terms -> TacticAst.Reduce (loc, kind, Some (terms, pat)))
+ | kind = reduction_kind; where = IDENT ; IDENT "at" ; pat = term ->
+ TacticAst.ReduceAt (loc, kind, where, pat)
| [ IDENT "reflexivity" ] ->
TacticAst.Reflexivity loc
| [ IDENT "replace" ];
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