GrafiteAst.Contradiction loc
| IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
GrafiteAst.Cut (loc, ident, t)
- | IDENT "decompose"; types = OPT ident_list0; what = OPT IDENT;
- idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
- let types = match types with None -> [] | Some types -> types in
+ | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
let idents = match idents with None -> [] | Some idents -> idents in
- let to_spec id = GrafiteAst.Ident id in
- GrafiteAst.Decompose (loc, List.rev_map to_spec types, what, idents)
+ GrafiteAst.Decompose (loc, idents)
| IDENT "demodulate" -> GrafiteAst.Demodulate loc
| IDENT "destruct"; t = tactic_term ->
GrafiteAst.Destruct (loc, t)
GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
| "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
defs = CicNotationParser.let_defs ->
+ (* In case of mutual definitions here we produce just
+ the syntax tree for the first one. The others will be
+ generated from the completely specified term just before
+ insertion in the environment. We use the flavour
+ `MutualDefinition to rememer this. *)
let name,ty =
match defs with
| (params,(Ast.Ident (name, None), Some ty),_,_) :: _ ->
| _ -> assert false
in
let body = Ast.Ident (name,None) in
- GrafiteAst.Obj (loc, Ast.Theorem(`Definition, name, ty,
- Some (Ast.LetRec (ind_kind, defs, body))))
+ let flavour =
+ if List.length defs = 1 then
+ `Definition
+ else
+ `MutualDefinition
+ in
+ GrafiteAst.Obj (loc, Ast.Theorem(flavour, name, ty,
+ Some (Ast.LetRec (ind_kind, defs, body))))
| IDENT "inductive"; spec = inductive_spec ->
let (params, ind_types) = spec in
GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
(loc,GrafiteAst.Include (iloc,buri))))
| scom = lexicon_command ; SYMBOL "." ->
fun ~include_paths status ->
- let status = LexiconEngine.eval_command status scom in
+ let status = LexiconEngine.eval_command status scom in
status,LNone loc
| EOI -> raise End_of_file
]