From 55ce117e8083477593cf1ff2e51a3641c7973830 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Tue, 13 Feb 2007 13:48:12 +0000 Subject: Imported Upstream version 8.1+dfsg --- parsing/g_constr.ml4 | 6 +- parsing/g_decl_mode.ml4 | 143 +++++++++++++++++++++++++++++++++++---------- parsing/g_natsyntaxnew.mli | 11 ---- parsing/g_tactic.ml4 | 3 +- parsing/g_vernac.ml4 | 10 ++-- parsing/g_zsyntaxnew.mli | 11 ---- parsing/ppdecl_proof.ml | 73 +++++++++++++---------- parsing/pptactic.ml | 3 +- parsing/ppvernac.ml | 18 +++--- parsing/printer.ml | 41 ++++++------- parsing/printer.mli | 9 ++- parsing/q_coqast.ml4 | 4 +- parsing/tactic_printer.ml | 16 ++--- 13 files changed, 210 insertions(+), 138 deletions(-) delete mode 100644 parsing/g_natsyntaxnew.mli delete mode 100644 parsing/g_zsyntaxnew.mli (limited to 'parsing') diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 130c6804..9163f3c1 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: g_constr.ml4 9226 2006-10-09 16:11:01Z herbelin $ *) +(* $Id: g_constr.ml4 9562 2007-01-31 09:00:36Z msozeau $ *) open Pcoq open Constr @@ -249,8 +249,8 @@ GEXTEND Gram ; fixannot: [ [ "{"; IDENT "struct"; id=name; "}" -> (Some id, CStructRec) - | "{"; IDENT "wf"; id=name; rel=lconstr; "}" -> (Some id, CWfRec rel) - | "{"; IDENT "measure"; id=name; rel=lconstr; "}" -> (Some id, CMeasureRec rel) + | "{"; IDENT "wf"; rel=constr; id=name; "}" -> (Some id, CWfRec rel) + | "{"; IDENT "measure"; rel=constr; id=name; "}" -> (Some id, CMeasureRec rel) | -> (None, CStructRec) ] ] ; diff --git a/parsing/g_decl_mode.ml4 b/parsing/g_decl_mode.ml4 index 8d7fd1f1..5c7b40af 100644 --- a/parsing/g_decl_mode.ml4 +++ b/parsing/g_decl_mode.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id:$ *) +(* $Id$ *) (*i camlp4deps: "parsing/grammar.cma" i*) open Decl_expr @@ -50,18 +50,26 @@ GLOBAL: proof_instr; | c=constr -> {st_label=Anonymous;st_it=This c} ] ]; - justification : - [[ -> Automated [] - | IDENT "by"; l=LIST1 constr SEP "," -> Automated l - | IDENT "by"; IDENT "tactic"; tac=tactic -> By_tactic tac ]] + justification_items : + [[ -> Some [] + | IDENT "by"; l=LIST1 constr SEP "," -> Some l + | IDENT "by"; "*" -> None ]] + ; + justification_method : + [[ -> None + | "using"; tac = tactic -> Some tac ]] ; simple_cut_or_thesis : [[ ls = statement_or_thesis; - j=justification -> {cut_stat=ls;cut_by=j} ]] + j = justification_items; + taco = justification_method + -> {cut_stat=ls;cut_by=j;cut_using=taco} ]] ; simple_cut : [[ ls = statement; - j=justification -> {cut_stat=ls;cut_by=j} ]] + j = justification_items; + taco = justification_method + -> {cut_stat=ls;cut_by=j;cut_using=taco} ]] ; elim_type: [[ IDENT "induction" -> ET_Induction @@ -76,10 +84,15 @@ GLOBAL: proof_instr; elim_obj: [[ IDENT "on"; c=constr -> Real c | IDENT "of"; c=simple_cut -> Virtual c ]] - ; + ; elim_step: - [[ IDENT "consider" ; h=vars ; IDENT "from" ; c=constr -> Pconsider (c,h) - | IDENT "per"; et=elim_type; obj=elim_obj -> Pper (et,obj)]] + [[ IDENT "consider" ; + h=consider_vars ; IDENT "from" ; c=constr -> Pconsider (c,h) + | IDENT "per"; et=elim_type; obj=elim_obj -> Pper (et,obj) + | IDENT "suffices"; ls=suff_clause; + j = justification_items; + taco = justification_method + -> Psuffices {cut_stat=ls;cut_by=j;cut_using=taco} ]] ; rew_step : [[ "~=" ; c=simple_cut -> (Rhs,c) @@ -106,46 +119,112 @@ GLOBAL: proof_instr; [[ id=loc_id -> id None ; | id=loc_id ; ":" ; c=constr -> id (Some c)]] ; - vars: + consider_vars: [[ name=hyp -> [Hvar name] - | name=hyp; ","; v=vars -> (Hvar name) :: v - | name=hyp; IDENT "be"; - IDENT "such"; IDENT "that"; h=hyps -> (Hvar name)::h + | name=hyp; ","; v=consider_vars -> (Hvar name) :: v | name=hyp; - IDENT "such"; IDENT "that"; h=hyps -> (Hvar name)::h + IDENT "such"; IDENT "that"; h=consider_hyps -> (Hvar name)::h ]] ; - hyps: - [[ IDENT "we"; IDENT "have"; v=vars -> v - | st=statement; IDENT "and"; h=hyps -> Hprop st::h - | st=statement; IDENT "and"; v=vars -> Hprop st::v + consider_hyps: + [[ st=statement; IDENT "and"; h=consider_hyps -> Hprop st::h + | st=statement; IDENT "and"; + IDENT "consider" ; v=consider_vars -> Hprop st::v | st=statement -> [Hprop st] ]] + ; + assume_vars: + [[ name=hyp -> [Hvar name] + | name=hyp; ","; v=assume_vars -> (Hvar name) :: v + | name=hyp; + IDENT "such"; IDENT "that"; h=assume_hyps -> (Hvar name)::h + ]] ; - vars_or_thesis: + assume_hyps: + [[ st=statement; IDENT "and"; h=assume_hyps -> Hprop st::h + | st=statement; IDENT "and"; + IDENT "we"; IDENT "have" ; v=assume_vars -> Hprop st::v + | st=statement -> [Hprop st] + ]] + ; + assume_clause: + [[ IDENT "we" ; IDENT "have" ; v=assume_vars -> v + | h=assume_hyps -> h ]] + ; + suff_vars: + [[ name=hyp; IDENT "to"; IDENT "show" ; c = constr_or_thesis -> + [Hvar name],c + | name=hyp; ","; v=suff_vars -> + let (q,c) = v in ((Hvar name) :: q),c + | name=hyp; + IDENT "such"; IDENT "that"; h=suff_hyps -> + let (q,c) = h in ((Hvar name) :: q),c + ]]; + suff_hyps: + [[ st=statement; IDENT "and"; h=suff_hyps -> + let (q,c) = h in (Hprop st::q),c + | st=statement; IDENT "and"; + IDENT "to" ; IDENT "have" ; v=suff_vars -> + let (q,c) = v in (Hprop st::q),c + | st=statement; IDENT "to"; IDENT "show" ; c = constr_or_thesis -> + [Hprop st],c + ]] + ; + suff_clause: + [[ IDENT "to" ; IDENT "have" ; v=suff_vars -> v + | h=suff_hyps -> h ]] + ; + let_vars: + [[ name=hyp -> [Hvar name] + | name=hyp; ","; v=let_vars -> (Hvar name) :: v + | name=hyp; IDENT "be"; + IDENT "such"; IDENT "that"; h=let_hyps -> (Hvar name)::h + ]] + ; + let_hyps: + [[ st=statement; IDENT "and"; h=let_hyps -> Hprop st::h + | st=statement; IDENT "and"; "let"; v=let_vars -> Hprop st::v + | st=statement -> [Hprop st] + ]]; + given_vars: + [[ name=hyp -> [Hvar name] + | name=hyp; ","; v=given_vars -> (Hvar name) :: v + | name=hyp; IDENT "such"; IDENT "that"; h=given_hyps -> (Hvar name)::h + ]] + ; + given_hyps: + [[ st=statement; IDENT "and"; h=given_hyps -> Hprop st::h + | st=statement; IDENT "and"; IDENT "given"; v=given_vars -> Hprop st::v + | st=statement -> [Hprop st] + ]]; + suppose_vars: [[name=hyp -> [Hvar name] - |name=hyp; ","; v=vars_or_thesis -> (Hvar name) :: v + |name=hyp; ","; v=suppose_vars -> (Hvar name) :: v |name=hyp; OPT[IDENT "be"]; - IDENT "such"; IDENT "that"; h=hyps_or_thesis -> (Hvar name)::h + IDENT "such"; IDENT "that"; h=suppose_hyps -> (Hvar name)::h ]] ; - hyps_or_thesis: - [[ IDENT "we"; IDENT "have"; v=vars_or_thesis -> v - | st=statement_or_thesis; IDENT "and"; h=hyps_or_thesis -> Hprop st::h - | st=statement_or_thesis; IDENT "and"; v=vars_or_thesis -> Hprop st::v - | st=statement_or_thesis -> [Hprop st]; + suppose_hyps: + [[ st=statement_or_thesis; IDENT "and"; h=suppose_hyps -> Hprop st::h + | st=statement_or_thesis; IDENT "and"; IDENT "we"; IDENT "have"; + v=suppose_vars -> Hprop st::v + | st=statement_or_thesis -> [Hprop st] ]] ; + suppose_clause: + [[ IDENT "we"; IDENT "have"; v=suppose_vars -> v; + | h=suppose_hyps -> h ]] + ; intro_step: - [[ IDENT "suppose" ; h=hyps -> Psuppose h + [[ IDENT "suppose" ; h=assume_clause -> Psuppose h | IDENT "suppose" ; IDENT "it"; IDENT "is" ; c=pattern LEVEL "0" ; po=OPT[ IDENT "with"; p=LIST1 hyp -> p ] ; - ho=OPT[ IDENT "and" ; h=hyps_or_thesis -> h ] -> + ho=OPT[ IDENT "and" ; h=suppose_clause -> h ] -> Pcase (none_is_empty po,c,none_is_empty ho) - | "let" ; v=vars -> Plet v + | "let" ; v=let_vars -> Plet v | IDENT "take"; witnesses = LIST1 constr SEP "," -> Ptake witnesses - | IDENT "assume"; h=hyps -> Passume h - | IDENT "given"; h=vars -> Pgiven h + | IDENT "assume"; h=assume_clause -> Passume h + | IDENT "given"; h=given_vars -> Pgiven h | IDENT "define"; id=ident; args=LIST0 hyp; "as"; body=constr -> Pdefine(id,args,body) | IDENT "reconsider"; id=ident; "as" ; typ=constr -> Pcast (This id,typ) diff --git a/parsing/g_natsyntaxnew.mli b/parsing/g_natsyntaxnew.mli deleted file mode 100644 index 97fb8791..00000000 --- a/parsing/g_natsyntaxnew.mli +++ /dev/null @@ -1,11 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* TacAssumption | IDENT "exact"; c = constr -> TacExact c | IDENT "exact_no_check"; c = constr -> TacExactNoCheck c + | IDENT "vm_cast_no_check"; c = constr -> TacVmCastNoCheck c | IDENT "apply"; cl = constr_with_bindings -> TacApply cl | IDENT "elim"; cl = constr_with_bindings; el = OPT eliminator -> diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 9bbdc1d4..9a98df80 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: g_vernac.ml4 9306 2006-10-28 18:28:19Z herbelin $ *) +(* $Id: g_vernac.ml4 9562 2007-01-31 09:00:36Z msozeau $ *) (*i camlp4deps: "parsing/grammar.cma" i*) open Pp @@ -264,8 +264,8 @@ GEXTEND Gram ; rec_annotation: [ [ "{"; IDENT "struct"; id=IDENT; "}" -> (Some (id_of_string id), CStructRec) - | "{"; IDENT "wf"; id=IDENT; rel=lconstr; "}" -> (Some (id_of_string id), CWfRec rel) - | "{"; IDENT "measure"; id=IDENT; rel=lconstr; "}" -> (Some (id_of_string id), CMeasureRec rel) + | "{"; IDENT "wf"; rel=constr; id=IDENT; "}" -> (Some (id_of_string id), CWfRec rel) + | "{"; IDENT "measure"; rel=constr; id=IDENT; "}" -> (Some (id_of_string id), CMeasureRec rel) | -> (None, CStructRec) ] ] ; @@ -459,7 +459,7 @@ GEXTEND Gram | IDENT "Implicit"; IDENT "Arguments"; qid = global; pos = OPT [ "["; l = LIST0 ident; "]" -> l ] -> let pos = option_map (List.map (fun id -> ExplByName id)) pos in - VernacDeclareImplicits (qid,pos) + VernacDeclareImplicits (true,qid,pos) | IDENT "Implicit"; ["Type" | IDENT "Types"]; idl = LIST1 identref; ":"; c = lconstr -> VernacReserve (idl,c) ] ] @@ -711,7 +711,7 @@ GEXTEND Gram refl = LIST1 class_rawexpr -> VernacBindScope (sc,refl) | IDENT "Arguments"; IDENT "Scope"; qid = global; - "["; scl = LIST0 opt_scope; "]" -> VernacArgumentsScope (qid,scl) + "["; scl = LIST0 opt_scope; "]" -> VernacArgumentsScope (true,qid,scl) | IDENT "Infix"; local = locality; op = ne_string; ":="; p = global; diff --git a/parsing/g_zsyntaxnew.mli b/parsing/g_zsyntaxnew.mli deleted file mode 100644 index 5168722e..00000000 --- a/parsing/g_zsyntaxnew.mli +++ /dev/null @@ -1,11 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* mt () | Name id -> pr_id id ++ spc () ++ str ":" ++ spc () -let pr_justification env = function - Automated [] -> mt () - | Automated (_::_ as l) -> +let pr_justification_items env = function + Some [] -> mt () + | Some (_::_ as l) -> spc () ++ str "by" ++ spc () ++ prlist_with_sep (fun () -> str ",") (pr_constr env) l - | By_tactic tac -> - spc () ++ str "by" ++ spc () ++ str "tactic" ++ pr_tac env tac + | None -> spc () ++ str "by *" + +let pr_justification_method env = function + None -> mt () + | Some tac -> + spc () ++ str "using" ++ pr_tac env tac let pr_statement pr_it env st = pr_label st.st_label ++ pr_it env st.st_it @@ -41,8 +45,9 @@ let pr_or_thesis pr_this env = function | This c -> pr_this env c let pr_cut pr_it env c = - hov 1 (pr_statement pr_it env c.cut_stat) ++ - pr_justification env c.cut_by + hov 1 (pr_it env c.cut_stat) ++ + pr_justification_items env c.cut_by ++ + pr_justification_method env c.cut_using let type_or_thesis = function Thesis _ -> Term.mkProp @@ -50,24 +55,24 @@ let type_or_thesis = function let _I x = x -let rec print_hyps pconstr gtyp env _and _be hyps = - let _andp = if _and then str "and" ++spc () else mt () in +let rec print_hyps pconstr gtyp env sep _be _have hyps = + let pr_sep = if sep then str "and" ++ spc () else mt () in match hyps with (Hvar _ ::_) as rest -> - spc () ++ _andp ++ str "we have" ++ - print_vars pconstr gtyp env false _be rest + spc () ++ pr_sep ++ str _have ++ + print_vars pconstr gtyp env false _be _have rest | Hprop st :: rest -> begin let nenv = match st.st_label with Anonymous -> env | Name id -> Environ.push_named (id,None,gtyp st.st_it) env in - spc() ++ _andp ++ pr_statement pconstr env st ++ - print_hyps pconstr gtyp nenv true _be rest + spc() ++ pr_sep ++ pr_statement pconstr env st ++ + print_hyps pconstr gtyp nenv true _be _have rest end | [] -> mt () -and print_vars pconstr gtyp env _and _be vars = +and print_vars pconstr gtyp env sep _be _have vars = match vars with Hvar st :: rest -> begin @@ -75,26 +80,30 @@ and print_vars pconstr gtyp env _and _be vars = match st.st_label with Anonymous -> anomaly "anonymous variable" | Name id -> Environ.push_named (id,None,st.st_it) env in - let _andp = if _and then pr_coma () else mt () in - spc() ++ _andp ++ + let pr_sep = if sep then pr_coma () else mt () in + spc() ++ pr_sep ++ pr_statement pr_constr env st ++ - print_vars pconstr gtyp nenv true _be rest + print_vars pconstr gtyp nenv true _be _have rest end | (Hprop _ :: _) as rest -> let _st = if _be then str "be such that" else str "such that" in - spc() ++ _st ++ print_hyps pconstr gtyp env false _be rest + spc() ++ _st ++ print_hyps pconstr gtyp env false _be _have rest | [] -> mt () +let pr_suffices_clause env (hyps,c) = + print_hyps pr_constr _I env false false "to have" hyps ++ spc () ++ + str "to show" ++ spc () ++ pr_or_thesis pr_constr env c + let pr_elim_type = function ET_Case_analysis -> str "cases" | ET_Induction -> str "induction" let pr_casee env =function Real c -> str "on" ++ spc () ++ pr_constr env c - | Virtual cut -> str "of" ++ spc () ++ pr_cut pr_constr env cut + | Virtual cut -> str "of" ++ spc () ++ pr_cut (pr_statement pr_constr) env cut let pr_side = function Lhs -> str "=~" @@ -109,30 +118,32 @@ let rec pr_bare_proof_instr _then _thus env = function begin match _then,_thus with false,false -> str "have" ++ spc () ++ - pr_cut (pr_or_thesis pr_constr) env c + pr_cut (pr_statement (pr_or_thesis pr_constr)) env c | false,true -> str "thus" ++ spc () ++ - pr_cut (pr_or_thesis pr_constr) env c + pr_cut (pr_statement (pr_or_thesis pr_constr)) env c | true,false -> str "then" ++ spc () ++ - pr_cut (pr_or_thesis pr_constr) env c + pr_cut (pr_statement (pr_or_thesis pr_constr)) env c | true,true -> str "hence" ++ spc () ++ - pr_cut (pr_or_thesis pr_constr) env c + pr_cut (pr_statement (pr_or_thesis pr_constr)) env c end + | Psuffices c -> + str "suffices" ++ pr_cut pr_suffices_clause env c | Prew (sid,c) -> (if _thus then str "thus" else str " ") ++ spc () ++ - pr_side sid ++ spc () ++ pr_cut pr_constr env c + pr_side sid ++ spc () ++ pr_cut (pr_statement pr_constr) env c | Passume hyps -> - str "assume" ++ print_hyps pr_constr _I env false false hyps + str "assume" ++ print_hyps pr_constr _I env false false "we have" hyps | Plet hyps -> - str "let" ++ print_vars pr_constr _I env false true hyps + str "let" ++ print_vars pr_constr _I env false true "let" hyps | Pclaim st -> str "claim" ++ spc () ++ pr_statement pr_constr env st | Pfocus st -> str "focus on" ++ spc () ++ pr_statement pr_constr env st | Pconsider (id,hyps) -> - str "consider" ++ print_vars pr_constr _I env false false hyps + str "consider" ++ print_vars pr_constr _I env false false "consider" hyps ++ spc () ++ str "from " ++ pr_constr env id | Pgiven hyps -> - str "given" ++ print_vars pr_constr _I env false false hyps + str "given" ++ print_vars pr_constr _I env false false "given" hyps | Ptake witl -> str "take" ++ spc () ++ prlist_with_sep pr_coma (pr_constr env) witl @@ -148,7 +159,7 @@ let rec pr_bare_proof_instr _then _thus env = function str "as" ++ (pr_constr env typ) | Psuppose hyps -> str "suppose" ++ - print_hyps pr_constr _I env false false hyps + print_hyps pr_constr _I env false false "we have" hyps | Pcase (params,pat,hyps) -> str "suppose it is" ++ spc () ++ pr_pat pat ++ (if params = [] then mt () else @@ -160,7 +171,7 @@ let rec pr_bare_proof_instr _then _thus env = function (if hyps = [] then mt () else (spc () ++ str "and" ++ print_hyps (pr_or_thesis pr_constr) type_or_thesis - env false false hyps)) + env false false "we have" hyps)) | Pper (et,c) -> str "per" ++ spc () ++ pr_elim_type et ++ spc () ++ pr_casee env c diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index c7e1db60..c68a2d6f 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pptactic.ml 9319 2006-10-30 12:41:21Z barras $ *) +(* $Id: pptactic.ml 9551 2007-01-29 15:13:35Z bgregoir $ *) open Pp open Names @@ -652,6 +652,7 @@ and pr_atom1 = function | TacAssumption as t -> pr_atom0 t | TacExact c -> hov 1 (str "exact" ++ pr_constrarg c) | TacExactNoCheck c -> hov 1 (str "exact_no_check" ++ pr_constrarg c) + | TacVmCastNoCheck c -> hov 1 (str "vm_cast_no_check" ++ pr_constrarg c) | TacApply cb -> hov 1 (str "apply" ++ spc () ++ pr_with_bindings cb) | TacElim (cb,cbo) -> hov 1 (str "elim" ++ pr_arg pr_with_bindings cb ++ diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index f86b5708..f9b8c425 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ppvernac.ml 9154 2006-09-20 17:18:18Z corbinea $ *) +(* $Id: ppvernac.ml 9562 2007-01-31 09:00:36Z msozeau $ *) open Pp open Names @@ -447,7 +447,7 @@ let rec pr_vernac = function | VernacBindScope (sc,cll) -> str"Bind Scope" ++ spc () ++ str sc ++ spc() ++ str "with " ++ prlist_with_sep spc pr_class_rawexpr cll - | VernacArgumentsScope (q,scl) -> let pr_opt_scope = function + | VernacArgumentsScope (local,q,scl) -> let pr_opt_scope = function | None -> str"_" | Some sc -> str sc in str"Arguments Scope" ++ spc() ++ pr_reference q ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]" @@ -570,11 +570,11 @@ let rec pr_vernac = function spc() ++ str "{struct " ++ pr_name name ++ str"}" else mt() | CWfRec c -> - spc() ++ str "{wf " ++ pr_name name ++ spc() ++ - pr_lconstr_expr c ++ str"}" + spc() ++ str "{wf " ++ pr_lconstr_expr c ++ spc() ++ + pr_name name ++ str"}" | CMeasureRec c -> - spc() ++ str "{measure " ++ pr_name name ++ spc() ++ - pr_lconstr_expr c ++ str"}" + spc() ++ str "{measure " ++ pr_lconstr_expr c ++ spc() ++ + pr_name name ++ str"}" in pr_id id ++ pr_binders_arg bl ++ annot ++ spc() ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_ @@ -741,11 +741,11 @@ let rec pr_vernac = function (str"Notation " ++ pr_locality local ++ pr_id id ++ str" :=" ++ pr_constrarg c ++ pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else [])) - | VernacDeclareImplicits (q,None) -> + | VernacDeclareImplicits (local,q,None) -> hov 2 (str"Implicit Arguments" ++ spc() ++ pr_reference q) - | VernacDeclareImplicits (q,Some l) -> + | VernacDeclareImplicits (local,q,Some l) -> let r = Nametab.global q in - Impargs.declare_manual_implicits r l; + Impargs.declare_manual_implicits local r l; let imps = Impargs.implicits_of_global r in hov 1 (str"Implicit Arguments" ++ spc() ++ pr_reference q ++ spc() ++ str"[" ++ prlist_with_sep sep (pr_explanation imps) l ++ str"]") diff --git a/parsing/printer.ml b/parsing/printer.ml index c0a98809..6fb492ae 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: printer.ml 9164 2006-09-23 09:36:05Z herbelin $ *) +(* $Id: printer.ml 9573 2007-01-31 20:18:18Z notin $ *) open Pp open Util @@ -29,7 +29,11 @@ open Pfedit open Ppconstr open Constrextern -let emacs_str s = if !Options.print_emacs then s else "" +let emacs_str s alts = + match !Options.print_emacs, !Options.print_emacs_safechar with + | true, true -> alts + | true , false -> s + | false,_ -> "" (**********************************************************************) (** Terms *) @@ -210,7 +214,7 @@ let pr_context_limit n env = else let pidt = pr_var_decl env d in (i+1, (pps ++ fnl () ++ - str (emacs_str (String.make 1 (Char.chr 253))) ++ + str (emacs_str (String.make 1 (Char.chr 253)) "") ++ pidt))) env ~init:(0,(mt ())) in @@ -219,7 +223,7 @@ let pr_context_limit n env = (fun env d pps -> let pnat = pr_rel_decl env d in (pps ++ fnl () ++ - str (emacs_str (String.make 1 (Char.chr 253))) ++ + str (emacs_str (String.make 1 (Char.chr 253)) "") ++ pnat)) env ~init:(mt ()) in @@ -231,25 +235,15 @@ let pr_context_of env = match Options.print_hyps_limit () with (* display goal parts (Proof mode) *) -let pr_restricted_named_context among env = - hv 0 (fold_named_context - (fun env ((id,_,_) as d) pps -> - if true || Idset.mem id among then - pps ++ - fnl () ++ str (emacs_str (String.make 1 (Char.chr 253))) ++ - pr_var_decl env d - else - pps) - env ~init:(mt ())) - let pr_subgoal_metas metas env= let pr_one (meta,typ) = str "?" ++ int meta ++ str " : " ++ hov 0 (pr_ltype_env_at_top env typ) ++ fnl () ++ - str (emacs_str (String.make 1 (Char.chr 253))) in + str (emacs_str (String.make 1 (Char.chr 253)) "") in hv 0 (prlist_with_sep mt pr_one metas) (* display complete goal *) + let pr_goal g = let env = evar_env g in let preamb,penv,pc = @@ -258,14 +252,14 @@ let pr_goal g = pr_context_of env, pr_ltype_env_at_top env g.evar_concl else - let {pm_subgoals=metas;pm_hyps=among} = get_info g in + let {pm_subgoals=metas} = get_info g in (str " *** Declarative Mode ***" ++ fnl ()++fnl ()), - pr_restricted_named_context among env, + pr_context_of env, pr_subgoal_metas metas env in preamb ++ str" " ++ hv 0 (penv ++ fnl () ++ - str (emacs_str (String.make 1 (Char.chr 253))) ++ + str (emacs_str (String.make 1 (Char.chr 253)) "") ++ str "============================" ++ fnl () ++ str" " ++ pc) ++ fnl () @@ -273,7 +267,7 @@ let pr_goal g = let pr_concl n g = let env = evar_env g in let pc = pr_ltype_env_at_top env g.evar_concl in - str (emacs_str (String.make 1 (Char.chr 253))) ++ + str (emacs_str (String.make 1 (Char.chr 253)) "") ++ str "subgoal " ++ int n ++ str " is:" ++ cut () ++ str" " ++ pc @@ -425,6 +419,13 @@ let pr_prim_rule = function | Rename (id1,id2) -> (str "rename " ++ pr_id id1 ++ str " into " ++ pr_id id2) + | Change_evars -> + (* This is internal tactic and cannot be replayed at user-level. + Function pr_rule_dot below is used when we want to hide + Change_evars *) + str "Evar change" + + (* Backwards compatibility *) let prterm = pr_lconstr diff --git a/parsing/printer.mli b/parsing/printer.mli index 6795889c..86af523f 100644 --- a/parsing/printer.mli +++ b/parsing/printer.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: printer.mli 9249 2006-10-19 07:46:03Z herbelin $ i*) +(*i $Id: printer.mli 9385 2006-11-17 15:14:14Z courtieu $ i*) (*i*) open Pp @@ -98,8 +98,11 @@ val pr_evars_int : int -> (evar * evar_info) list -> std_ppcmds val pr_prim_rule : prim_rule -> std_ppcmds (* Emacs/proof general support *) - -val emacs_str : string -> string +(* (emacs_str s alts) outputs + - s if emacs mode & unicode allowed, + - alts if emacs mode and & unicode not allowed + - nothing otherwise *) +val emacs_str : string -> string -> string (* Backwards compatibility *) diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 23d24497..23787f4c 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: q_coqast.ml4 9315 2006-10-29 21:53:30Z barras $ *) +(* $Id: q_coqast.ml4 9551 2007-01-29 15:13:35Z bgregoir $ *) open Util open Names @@ -271,6 +271,8 @@ let rec mlexpr_of_atomic_tactic = function <:expr< Tacexpr.TacExact $mlexpr_of_constr c$ >> | Tacexpr.TacExactNoCheck c -> <:expr< Tacexpr.TacExactNoCheck $mlexpr_of_constr c$ >> + | Tacexpr.TacVmCastNoCheck c -> + <:expr< Tacexpr.TacVmCastNoCheck $mlexpr_of_constr c$ >> | Tacexpr.TacApply cb -> <:expr< Tacexpr.TacApply $mlexpr_of_constr_with_binding cb$ >> | Tacexpr.TacElim (cb,cbo) -> diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml index 6ea1c97e..1fef688c 100644 --- a/parsing/tactic_printer.ml +++ b/parsing/tactic_printer.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tactic_printer.ml 9244 2006-10-16 17:11:44Z barras $ *) +(* $Id: tactic_printer.ml 9593 2007-02-05 13:58:52Z corbinea $ *) open Pp open Util @@ -39,11 +39,6 @@ let pr_rule = function end | Daimon -> str "" | Decl_proof _ -> str "proof" - | Change_evars -> - (* This is internal tactic and cannot be replayed at user-level. - Function pr_rule_dot below is used when we want to hide - Change_evars *) - str "Evar change" let uses_default_tac = function | Nested(Tactic(_,dflt),_) -> dflt @@ -51,7 +46,7 @@ let uses_default_tac = function (* Does not print change of evars *) let pr_rule_dot = function - | Change_evars -> mt () + | Prim Change_evars -> mt () | r -> pr_rule r ++ if uses_default_tac r then str "..." else str"." @@ -93,7 +88,10 @@ let rec print_decl_script tac_printer nochange sigma pf = else pr_change pf.goal) ++ fnl () - | Some (Daimon,_) -> mt () + | Some (Daimon,[]) -> mt () + | Some (Prim Change_evars,[next]) -> + (* ignore evar changes *) + print_decl_script tac_printer nochange sigma next | Some (Nested(Proof_instr (opened,instr),_) as rule,subprfs) -> begin match instr.instr,subprfs with @@ -213,8 +211,6 @@ let rec print_info_script sigma osign pf = let {evar_hyps=sign; evar_concl=cl} = pf.goal in match pf.ref with | None -> (mt ()) - | Some(Change_evars,[spf]) -> - print_info_script sigma osign spf | Some(r,spfl) -> (pr_rule r ++ match spfl with -- cgit v1.2.3