From: Andrea Asperti Date: Thu, 20 Oct 2011 15:49:59 +0000 (+0000) Subject: QED takes a boolean parameter governing indexing. X-Git-Tag: make_still_working~2166 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=59e3ddd15ee1983027e8929c073b06a80d523875;p=helm.git QED takes a boolean parameter governing indexing. Syntax to avoid indexing is qed- --- diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml index 6b5344f58..e96cf1bbc 100644 --- a/matita/components/grafite/grafiteAst.ml +++ b/matita/components/grafite/grafiteAst.ml @@ -105,7 +105,7 @@ type command = | 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 - | NQed of loc + | NQed of loc * bool (* ex lexicon commands *) | Alias of loc * alias_spec (** parameters, name, type, fields *) diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index 9c0f456b2..59821ac09 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -492,7 +492,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = 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 @@ -527,7 +527,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = let obj = uri,height,[],[],obj_kind in let old_status = status in let status = NCicLibrary.add_obj status obj in - let index_obj = + let index_obj = index && match obj_kind with NCic.Constant (_,_,_,_,(_,`Example,_)) | NCic.Fixpoint (_,_,(_,`Example,_)) -> false @@ -593,7 +593,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = 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"; *) @@ -618,7 +618,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = 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 @@ -645,7 +645,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = 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"; *) @@ -717,7 +717,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = 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") @@ -733,7 +733,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = 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 @@ -752,7 +752,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = 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) -> @@ -794,7 +794,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = (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] diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml index ff36dbe21..16bc6c32e 100644 --- a/matita/components/grafite_parser/grafiteParser.ml +++ b/matita/components/grafite_parser/grafiteParser.ml @@ -536,7 +536,10 @@ EXTEND ]]; 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> (* ≝ *); body = term -> body ] -> G.NObj (loc, N.Theorem (nflavour, name, typ, body,`Regular))