summary |
shortlog |
log |
commit | commitdiff |
tree
raw |
patch |
inline | side by side (from parent 1:
223f026)
Syntax to avoid indexing is qed-
| NUnivConstraint of loc * NUri.uri * NUri.uri
| NCopy of loc * string * NUri.uri * (NUri.uri * NUri.uri) list
| NCoercion of loc * string * bool * nterm * nterm * (string * nterm) * nterm
| NUnivConstraint of loc * NUri.uri * NUri.uri
| NCopy of loc * string * NUri.uri * (NUri.uri * NUri.uri) list
| NCoercion of loc * string * bool * nterm * nterm * (string * nterm) * nterm
(* ex lexicon commands *)
| Alias of loc * alias_spec
(** parameters, name, type, fields *)
(* ex lexicon commands *)
| Alias of loc * alias_spec
(** parameters, name, type, fields *)
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 _,_,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
| _ -> status))
(* XXX *)
with
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 discrimination principle"; *)
| _ -> status))
(* XXX *)
with _ -> (*HLog.warn "error in generating discrimination 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 (loc, indty) ->
if status#ng_mode <> `CommandMode then
| _ -> status)
| GrafiteAst.NDiscriminator (loc, indty) ->
if status#ng_mode <> `CommandMode then
it leftno status status#baseuri in
let _,_,menv,_,_ = obj in
(match menv with
it leftno status status#baseuri in
let _,_,menv,_,_ = obj in
(match menv 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,false))
| _ -> prerr_endline ("Discriminator: non empty metasenv");
status)
| GrafiteAst.NInverter (loc, name, indty, selection, sort) ->
| _ -> prerr_endline ("Discriminator: non empty metasenv");
status)
| GrafiteAst.NInverter (loc, name, indty, selection, sort) ->
(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
+ if not b then prerr_endline "Should not index";
+ 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))