2. added a boolean to qed to governe indexing
the syntax for disabling indexing is "qed-"
| Ast.List0 (_, None) -> Gramext.Slist0 s
| Ast.List1 (_, None) -> Gramext.Slist1 s
| Ast.List0 (_, Some l) ->
| Ast.List0 (_, None) -> Gramext.Slist0 s
| Ast.List1 (_, None) -> Gramext.Slist1 s
| Ast.List0 (_, Some l) ->
- Gramext.Slist0sep (s, gram_of_literal status l, true)
+ Gramext.Slist0sep (s, gram_of_literal status l)
| Ast.List1 (_, Some l) ->
| Ast.List1 (_, Some l) ->
- Gramext.Slist1sep (s, gram_of_literal status l, true)
+ Gramext.Slist1sep (s, gram_of_literal status l)
| _ -> assert false
in
[ Env (List.map Env.list_declaration p_names),
| _ -> assert false
in
[ Env (List.map Env.list_declaration p_names),
| NCoercion of loc * string *
(NotationPt.term * NotationPt.term *
(string * NotationPt.term) * NotationPt.term) option
| NCoercion of loc * string *
(NotationPt.term * NotationPt.term *
(string * NotationPt.term) * NotationPt.term) option
(* ex lexicon commands *)
| Alias of loc * alias_spec
(** parameters, name, type, fields *)
(* ex lexicon commands *)
| Alias of loc * alias_spec
(** parameters, name, type, fields *)
| NUnivConstraint (_) -> "not supported"
| NCoercion (_) -> "not supported"
| NObj (_,obj) -> NotationPp.pp_obj (NotationPp.pp_term status) obj
| NUnivConstraint (_) -> "not supported"
| NCoercion (_) -> "not supported"
| NObj (_,obj) -> NotationPp.pp_obj (NotationPp.pp_term status) obj
| NCopy (_,name,uri,map) ->
"copy " ^ name ^ " from " ^ NUri.string_of_uri uri ^ " with " ^
String.concat " and "
| NCopy (_,name,uri,map) ->
"copy " ^ name ^ " from " ^ NUri.string_of_uri uri ^ " with " ^
String.concat " and "
let mode = GrafiteAst.WithPreferences in (* MATITA 1.0: fixme *)
let aliases = GrafiteDisambiguate.aliases_for_objs status composites in
eval_alias status (mode,aliases)
let mode = GrafiteAst.WithPreferences in (* MATITA 1.0: fixme *)
let aliases = GrafiteDisambiguate.aliases_for_objs status composites in
eval_alias status (mode,aliases)
- | GrafiteAst.NQed loc ->
+ | GrafiteAst.NQed (loc,index) ->
if status#ng_mode <> `ProofMode then
raise (GrafiteTypes.Command_error "Not in proof mode")
else
if status#ng_mode <> `ProofMode then
raise (GrafiteTypes.Command_error "Not in proof mode")
else
let obj = uri,height,[],[],obj_kind in
let old_status = status in
let status = NCicLibrary.add_obj status obj in
let obj = uri,height,[],[],obj_kind in
let old_status = status in
let status = NCicLibrary.add_obj status obj in
+ let index_obj = index &&
match obj_kind with
NCic.Constant (_,_,_,_,(_,`Example,_))
| NCic.Fixpoint (_,_,(_,`Example,_)) -> false
match obj_kind with
NCic.Constant (_,_,_,_,(_,`Example,_))
| NCic.Fixpoint (_,_,(_,`Example,_)) -> false
let _,_,menv,_,_ = invobj in
(match menv with
[] -> eval_ncommand ~include_paths opts status
let _,_,menv,_,_ = invobj in
(match menv with
[] -> eval_ncommand ~include_paths opts status
- ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
+ ("",0,GrafiteAst.NQed (Stdpp.dummy_loc,false))
| _ -> status))
(* XXX *)
with _ -> (*HLog.warn "error in generating inversion principle"; *)
| _ -> status))
(* XXX *)
with _ -> (*HLog.warn "error in generating inversion principle"; *)
let status = status#set_stack ninitial_stack in
let status = subst_metasenv_and_fix_names status in
let status = status#set_ng_mode `ProofMode in
let status = status#set_stack ninitial_stack in
let status = subst_metasenv_and_fix_names status in
let status = status#set_ng_mode `ProofMode in
- eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
+ eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed (Stdpp.dummy_loc,false))
| GrafiteAst.NObj (loc,obj) ->
if status#ng_mode <> `CommandMode then
raise (GrafiteTypes.Command_error "Not in command mode")
| GrafiteAst.NObj (loc,obj) ->
if status#ng_mode <> `CommandMode then
raise (GrafiteTypes.Command_error "Not in command mode")
let status = status#set_ng_mode `ProofMode in
(match nmenv with
[] ->
let status = status#set_ng_mode `ProofMode in
(match nmenv with
[] ->
- eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
+ eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed (Stdpp.dummy_loc,true))
| _ -> status)
| GrafiteAst.NDiscriminator (_,_) -> assert false (*(loc, indty) ->
if status#ng_mode <> `CommandMode then
| _ -> status)
| GrafiteAst.NDiscriminator (_,_) -> assert false (*(loc, indty) ->
if status#ng_mode <> `CommandMode then
(match menv with
[] ->
eval_ncommand ~include_paths opts status
(match menv with
[] ->
eval_ncommand ~include_paths opts status
- ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
+ ("",0,GrafiteAst.NQed (Stdpp.dummy_loc,false))
| _ -> assert false)
| GrafiteAst.NUnivConstraint (loc,u1,u2) ->
eval_add_constraint status [`Type,u1] [`Type,u2]
| _ -> assert false)
| GrafiteAst.NUnivConstraint (loc,u1,u2) ->
eval_add_constraint status [`Type,u1] [`Type,u2]
]];
grafite_ncommand: [ [
]];
grafite_ncommand: [ [
- IDENT "qed" -> G.NQed loc
+ IDENT "qed" ; b = OPT SYMBOL "-" ->
+ let b = match b with None -> true | Some _ -> false in G.NQed (loc,b)
| nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
G.NObj (loc, N.Theorem (nflavour, name, typ, body,`Regular))
| nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
G.NObj (loc, N.Theorem (nflavour, name, typ, body,`Regular))
| Smeta (_, lt, _) -> List.for_all is_symbol_dummy lt
| Snterm e | Snterml (e, _) -> is_entry_dummy e
| Slist1 x | Slist0 x -> is_symbol_dummy x
| Smeta (_, lt, _) -> List.for_all is_symbol_dummy lt
| Snterm e | Snterml (e, _) -> is_entry_dummy e
| Slist1 x | Slist0 x -> is_symbol_dummy x
- | Slist1sep (x,y,_) | Slist0sep (x,y,_) -> is_symbol_dummy x && is_symbol_dummy y
+ | Slist1sep (x,y) | Slist0sep (x,y) -> is_symbol_dummy x && is_symbol_dummy y
| Sopt x -> is_symbol_dummy x
| Sself | Snext -> false
| Stree t -> is_tree_dummy t
| Sopt x -> is_symbol_dummy x
| Sself | Snext -> false
| Stree t -> is_tree_dummy t
let todo = visit_symbol symbol todo is_son in
Format.fprintf fmt "@]} @ ";
todo
let todo = visit_symbol symbol todo is_son in
Format.fprintf fmt "@]} @ ";
todo
- | Slist0sep (symbol,sep,_) ->
+ | Slist0sep (symbol,sep) ->
Format.fprintf fmt "[@[<hov2> ";
let todo = visit_symbol symbol todo is_son in
Format.fprintf fmt "{@[<hov2> ";
Format.fprintf fmt "[@[<hov2> ";
let todo = visit_symbol symbol todo is_son in
Format.fprintf fmt "{@[<hov2> ";
let todo = visit_symbol symbol todo is_son in
Format.fprintf fmt "@]}+ @ ";
todo
let todo = visit_symbol symbol todo is_son in
Format.fprintf fmt "@]}+ @ ";
todo
- | Slist1sep (symbol,sep,_) ->
+ | Slist1sep (symbol,sep) ->
let todo = visit_symbol symbol todo is_son in
Format.fprintf fmt "{@[<hov2> ";
let todo = visit_symbol sep todo is_son in
let todo = visit_symbol symbol todo is_son in
Format.fprintf fmt "{@[<hov2> ";
let todo = visit_symbol sep todo is_son in