`MutualDefinition to rememer this. *)
let name,ty =
match defs with
- | (params,(N.Ident (name, None), Some ty),_,_) :: _ ->
+ | (params,(N.Ident (name, None), ty),_,_) :: _ ->
+ let ty = match ty with Some ty -> ty | None -> N.Implicit in
let ty =
List.fold_right
(fun var ty -> N.Binder (`Pi,var,ty)
) params ty
in
name,ty
- | (_,(N.Ident (name, None), None),_,_) :: _ ->
- name, N.Implicit
| _ -> assert false
in
let body = N.Ident (name,None) in
| IDENT "nodefaults" -> G.IPNoDefaults
| IDENT "depth"; SYMBOL "="; depth = int -> G.IPDepth depth
| IDENT "level"; SYMBOL "="; level = int -> G.IPLevel level
+ | IDENT "comments" -> G.IPComments
+ | IDENT "coercions" -> G.IPCoercions
+ | IDENT "debug"; SYMBOL "="; debug = int -> G.IPDebug debug
] -> params
]
];
include_command: [ [
IDENT "include" ; path = QSTRING ->
- loc,path,false,L.WithPreferences
+ loc,path,true,L.WithPreferences
| IDENT "include" ; IDENT "source" ; path = QSTRING ->
- loc,path,true,L.WithPreferences
+ loc,path,false,L.WithPreferences
| IDENT "include'" ; path = QSTRING ->
- loc,path,false,L.WithoutPreferences
+ loc,path,true,L.WithoutPreferences
]];
grafite_command: [ [
let stm = G.Comment (loc, com) in
!grafite_callback status stm;
status, LSome stm
- | (iloc,fname,source,mode) = include_command ; SYMBOL "." ->
+ | (iloc,fname,normal,mode) = include_command ; SYMBOL "." ->
fun ?(never_include=false) ~include_paths status ->
let stm =
- G.Executable (loc, G.Command (loc, G.Include (iloc, source, fname)))
+ G.Executable (loc, G.Command (loc, G.Include (iloc, normal, fname)))
in
!grafite_callback status stm;
let _root, buri, fullpath, _rrelpath =
Librarian.baseuri_of_script ~include_paths fname
in
- let stm =
- G.Executable (loc, G.Command (loc, G.Include (iloc, source, buri)))
- in
let status =
if never_include then raise (NoInclusionPerformed fullpath)
else LE.eval_command status (L.Include (iloc,buri,mode,fullpath))
in
+ let stm =
+ G.Executable (loc, G.Command (loc, G.Include (iloc, normal, buri)))
+ in
status, LSome stm
| scom = lexicon_command ; SYMBOL "." ->
fun ?(never_include=false) ~include_paths status ->