From 208a0f7bfa5249f9795e6e225f309cbe715c0fad Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Tue, 21 Nov 2006 21:38:49 +0000 Subject: Imported Upstream version 8.1~gamma --- parsing/argextend.ml4 | 8 +- parsing/egrammar.ml | 25 ++++--- parsing/egrammar.mli | 5 +- parsing/g_constr.ml4 | 14 +++- parsing/g_decl_mode.ml4 | 171 ++++++++++++++++++++++++++++++++++++++++++ parsing/g_ltac.ml4 | 42 +++++++---- parsing/g_proofs.ml4 | 3 +- parsing/g_vernac.ml4 | 62 ++++++++++++---- parsing/g_xml.ml4 | 10 ++- parsing/pcoq.ml4 | 9 ++- parsing/pcoq.mli | 10 ++- parsing/ppconstr.ml | 15 ++-- parsing/ppdecl_proof.ml | 180 +++++++++++++++++++++++++++++++++++++++++++++ parsing/ppdecl_proof.mli | 2 + parsing/pptactic.ml | 19 ++--- parsing/ppvernac.ml | 21 ++++-- parsing/prettyp.ml | 17 ++++- parsing/printer.ml | 92 +++++++++++++++++------ parsing/printer.mli | 5 +- parsing/q_coqast.ml4 | 8 +- parsing/q_util.ml4 | 36 +++++++-- parsing/q_util.mli | 5 +- parsing/search.ml | 8 +- parsing/tacextend.ml4 | 9 ++- parsing/tactic_printer.ml | 162 ++++++++++++++++++++++++++++++++-------- parsing/tactic_printer.mli | 6 +- parsing/vernacextend.ml4 | 4 +- 27 files changed, 786 insertions(+), 162 deletions(-) create mode 100644 parsing/g_decl_mode.ml4 create mode 100644 parsing/ppdecl_proof.ml create mode 100644 parsing/ppdecl_proof.mli (limited to 'parsing') diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4 index 638a8d65..12c0ea1d 100644 --- a/parsing/argextend.ml4 +++ b/parsing/argextend.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: argextend.ml4 8976 2006-06-23 10:03:54Z herbelin $ *) +(* $Id: argextend.ml4 9265 2006-10-24 08:35:38Z herbelin $ *) open Genarg open Q_util @@ -213,7 +213,7 @@ EXTEND [ e = argtype; LIDENT "list" -> List0ArgType e | e = argtype; LIDENT "option" -> OptArgType e ] | "0" - [ e = LIDENT -> fst (interp_entry_name loc e) + [ e = LIDENT -> fst (interp_entry_name loc e "") | "("; e = argtype; ")" -> e ] ] ; argrule: @@ -221,7 +221,9 @@ EXTEND ; genarg: [ [ e = LIDENT; "("; s = LIDENT; ")" -> - let t, g = interp_entry_name loc e in (g, Some (s,t)) + let t, g = interp_entry_name loc e "" in (g, Some (s,t)) + | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> + let t, g = interp_entry_name loc e sep in (g, Some (s,t)) | s = STRING -> if String.length s > 0 && Util.is_letter s.[0] then Pcoq.lexer.Token.using ("", s); diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index 9ec7c532..07a0a65f 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: egrammar.ml 8926 2006-06-08 20:23:17Z herbelin $ *) +(* $Id: egrammar.ml 9333 2006-11-02 13:59:14Z barras $ *) open Pp open Util @@ -196,23 +196,24 @@ let find_index s t = if s <> t or n = None then raise Not_found; out_some n -let rec interp_entry_name up_level u s = +let rec interp_entry_name up_level s = let l = String.length s in if l > 8 & String.sub s 0 3 = "ne_" & String.sub s (l-5) 5 = "_list" then - let t, g = interp_entry_name up_level u (String.sub s 3 (l-8)) in + let t, g = interp_entry_name up_level (String.sub s 3 (l-8)) in List1ArgType t, Gramext.Slist1 g else if l > 5 & String.sub s (l-5) 5 = "_list" then - let t, g = interp_entry_name up_level u (String.sub s 0 (l-5)) in + let t, g = interp_entry_name up_level (String.sub s 0 (l-5)) in List0ArgType t, Gramext.Slist0 g else if l > 4 & String.sub s (l-4) 4 = "_opt" then - let t, g = interp_entry_name up_level u (String.sub s 0 (l-4)) in + let t, g = interp_entry_name up_level (String.sub s 0 (l-4)) in OptArgType t, Gramext.Sopt g else + let s = if s = "hyp" then "var" else s in try let i = find_index "tactic" s in ExtraArgType s, - if i=up_level then Gramext.Sself else - if i=up_level-1 then Gramext.Snext else + if up_level<>5 && i=up_level then Gramext.Sself else + if up_level<>5 && i=up_level-1 then Gramext.Snext else Gramext.Snterml(Pcoq.Gram.Entry.obj Tactic.tactic_expr,string_of_int i) with Not_found -> let e = @@ -228,16 +229,18 @@ let rec interp_entry_name up_level u s = let t = type_of_typed_entry e in t,Gramext.Snterm (Pcoq.Gram.Entry.obj o) -let make_vprod_item n univ = function +let make_vprod_item n = function | VTerm s -> (Gramext.Stoken (Lexer.terminal s), None) | VNonTerm (loc, nt, po) -> - let (etyp, e) = interp_entry_name n univ nt in + let (etyp, e) = interp_entry_name n nt in e, option_map (fun p -> (p,etyp)) po let get_tactic_entry n = if n = 0 then weaken_entry Tactic.simple_tactic, None - else if 1<=n && n<=5 then + else if n = 5 then + weaken_entry Tactic.binder_tactic, None + else if 1<=n && n<5 then weaken_entry Tactic.tactic_expr, Some (Gramext.Level (string_of_int n)) else error ("Invalid Tactic Notation level: "^(string_of_int n)) @@ -249,7 +252,7 @@ let head_is_ident = function VTerm _::_ -> true | _ -> false let add_tactic_entry (key,lev,prods,tac) = let univ = get_univ "tactic" in let entry, pos = get_tactic_entry lev in - let mkprod = make_vprod_item lev "tactic" in + let mkprod = make_vprod_item lev in let rules = if lev = 0 then begin if not (head_is_ident prods) then diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli index 31247044..5dda69ba 100644 --- a/parsing/egrammar.mli +++ b/parsing/egrammar.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: egrammar.mli 7732 2005-12-26 13:51:24Z herbelin $ i*) +(*i $Id: egrammar.mli 9147 2006-09-15 21:49:56Z herbelin $ i*) (*i*) open Util @@ -61,8 +61,7 @@ val get_extend_vernac_grammars : (* val reset_extend_grammars_v8 : unit -> unit *) -val interp_entry_name : int -> string -> string -> - entry_type * Token.t Gramext.g_symbol +val interp_entry_name : int -> string -> entry_type * Token.t Gramext.g_symbol val recover_notation_grammar : notation -> (precedence * tolerability list) -> notation_grammar diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index a1c0c9ae..130c6804 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 9043 2006-07-12 10:06:40Z herbelin $ *) +(* $Id: g_constr.ml4 9226 2006-10-09 16:11:01Z herbelin $ *) open Pcoq open Constr @@ -155,8 +155,14 @@ GEXTEND Gram [ "200" RIGHTA [ c = binder_constr -> c ] | "100" RIGHTA - [ c1 = operconstr; ":"; c2 = binder_constr -> CCast(loc,c1, CastConv DEFAULTcast,c2) - | c1 = operconstr; ":"; c2 = SELF -> CCast(loc,c1,CastConv DEFAULTcast,c2) ] + [ c1 = operconstr; "<:"; c2 = binder_constr -> + CCast(loc,c1, CastConv VMcast,c2) + | c1 = operconstr; "<:"; c2 = SELF -> + CCast(loc,c1, CastConv VMcast,c2) + | c1 = operconstr; ":";c2 = binder_constr -> + CCast(loc,c1, CastConv DEFAULTcast,c2) + | c1 = operconstr; ":"; c2 = SELF -> + CCast(loc,c1, CastConv DEFAULTcast,c2) ] | "99" RIGHTA [ ] | "90" RIGHTA [ c1 = operconstr; "->"; c2 = binder_constr -> CArrow(loc,c1,c2) @@ -287,7 +293,7 @@ GEXTEND Gram (match p with | CPatAtom (_, Some r) -> CPatCstr (loc, r, lp) | _ -> Util.user_err_loc - (cases_pattern_loc p, "compound_pattern", + (cases_pattern_expr_loc p, "compound_pattern", Pp.str "Constructor expected")) | p = pattern; "as"; id = ident -> CPatAlias (loc, p, id) ] diff --git a/parsing/g_decl_mode.ml4 b/parsing/g_decl_mode.ml4 new file mode 100644 index 00000000..8d7fd1f1 --- /dev/null +++ b/parsing/g_decl_mode.ml4 @@ -0,0 +1,171 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* [] + | Some l -> l + +GEXTEND Gram +GLOBAL: proof_instr; + thesis : + [[ "thesis" -> Plain + | "thesis"; "for"; i=ident -> (For i) + | "thesis"; "["; n=INT ;"]" -> (Sub (int_of_string n)) + ]]; + statement : + [[ i=ident ; ":" ; c=constr -> {st_label=Name i;st_it=c} + | i=ident -> {st_label=Anonymous; + st_it=Topconstr.CRef (Libnames.Ident (loc, i))} + | c=constr -> {st_label=Anonymous;st_it=c} + ]]; + constr_or_thesis : + [[ t=thesis -> Thesis t ] | + [ c=constr -> This c + ]]; + statement_or_thesis : + [ + [ t=thesis -> {st_label=Anonymous;st_it=Thesis t} ] + | + [ i=ident ; ":" ; cot=constr_or_thesis -> {st_label=Name i;st_it=cot} + | i=ident -> {st_label=Anonymous; + st_it=This (Topconstr.CRef (Libnames.Ident (loc, i)))} + | 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 ]] + ; + simple_cut_or_thesis : + [[ ls = statement_or_thesis; + j=justification -> {cut_stat=ls;cut_by=j} ]] + ; + simple_cut : + [[ ls = statement; + j=justification -> {cut_stat=ls;cut_by=j} ]] + ; + elim_type: + [[ IDENT "induction" -> ET_Induction + | IDENT "cases" -> ET_Case_analysis ]] + ; + block_type : + [[ IDENT "claim" -> B_claim + | IDENT "focus" -> B_focus + | IDENT "proof" -> B_proof + | et=elim_type -> B_elim et ]] + ; + 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)]] + ; + rew_step : + [[ "~=" ; c=simple_cut -> (Rhs,c) + | "=~" ; c=simple_cut -> (Lhs,c)]] + ; + cut_step: + [[ "then"; tt=elim_step -> Pthen tt + | "then"; c=simple_cut_or_thesis -> Pthen (Pcut c) + | IDENT "thus"; tt=rew_step -> Pthus (let s,c=tt in Prew (s,c)) + | IDENT "thus"; c=simple_cut_or_thesis -> Pthus (Pcut c) + | IDENT "hence"; c=simple_cut_or_thesis -> Phence (Pcut c) + | tt=elim_step -> tt + | tt=rew_step -> let s,c=tt in Prew (s,c); + | IDENT "have"; c=simple_cut_or_thesis -> Pcut c; + | IDENT "claim"; c=statement -> Pclaim c; + | IDENT "focus"; IDENT "on"; c=statement -> Pfocus c; + | "end"; bt = block_type -> Pend bt; + | IDENT "escape" -> Pescape ]] + ; + (* examiner s'il est possible de faire R _ et _ R pour R une relation qcq*) + loc_id: + [[ id=ident -> fun x -> (loc,(id,x)) ]]; + hyp: + [[ id=loc_id -> id None ; + | id=loc_id ; ":" ; c=constr -> id (Some c)]] + ; + 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; + IDENT "such"; IDENT "that"; h=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 + | st=statement -> [Hprop st] + ]] + ; + vars_or_thesis: + [[name=hyp -> [Hvar name] + |name=hyp; ","; v=vars_or_thesis -> (Hvar name) :: v + |name=hyp; OPT[IDENT "be"]; + IDENT "such"; IDENT "that"; h=hyps_or_thesis -> (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]; + ]] + ; + intro_step: + [[ IDENT "suppose" ; h=hyps -> 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 ] -> + Pcase (none_is_empty po,c,none_is_empty ho) + | "let" ; v=vars -> Plet v + | IDENT "take"; witnesses = LIST1 constr SEP "," -> Ptake witnesses + | IDENT "assume"; h=hyps -> Passume h + | IDENT "given"; h=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) + | IDENT "reconsider"; t=thesis; "as" ; typ=constr -> Pcast (Thesis t ,typ) + ]] + ; + emphasis : + [[ -> 0 + | "*" -> 1 + | "**" -> 2 + | "***" -> 3 + ]] + ; + bare_proof_instr: + [[ c = cut_step -> c ; + | i = intro_step -> i ]] + ; + proof_instr : + [[ e=emphasis;i=bare_proof_instr -> {emph=e;instr=i}]] + ; +END;; + + diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index c01c23b6..27ff8140 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: g_ltac.ml4 9037 2006-07-11 12:43:50Z herbelin $ *) +(* $Id: g_ltac.ml4 9333 2006-11-02 13:59:14Z barras $ *) open Pp open Util @@ -43,38 +43,34 @@ let tacarg_of_expr = function (* Tactics grammar rules *) GEXTEND Gram - GLOBAL: tactic Vernac_.command tactic_expr tactic_arg constr_may_eval; + GLOBAL: tactic Vernac_.command tactic_expr binder_tactic tactic_arg + constr_may_eval; tactic_expr: - [ "5" LEFTA - [ ta0 = tactic_expr; ";"; ta1 = tactic_expr -> TacThen (ta0, ta1) + [ "5" RIGHTA + [ te = binder_tactic -> te ] + | "4" LEFTA + [ ta0 = tactic_expr; ";"; ta1 = binder_tactic -> TacThen (ta0, ta1) + | ta0 = tactic_expr; ";"; ta1 = tactic_expr -> TacThen (ta0, ta1) | ta = tactic_expr; ";"; "["; lta = LIST0 OPT tactic_expr SEP "|"; "]" -> let lta = List.map (function None -> TacId [] | Some t -> t) lta in TacThens (ta, lta) ] - | "4" - [ ] | "3" RIGHTA [ IDENT "try"; ta = tactic_expr -> TacTry ta | IDENT "do"; n = int_or_var; ta = tactic_expr -> TacDo (n,ta) | IDENT "repeat"; ta = tactic_expr -> TacRepeat ta | IDENT "progress"; ta = tactic_expr -> TacProgress ta - | IDENT "info"; tc = tactic_expr -> TacInfo tc (*To do: put Abstract in Refiner*) | IDENT "abstract"; tc = NEXT -> TacAbstract (tc,None) | IDENT "abstract"; tc = NEXT; "using"; s = ident -> TacAbstract (tc,Some s) ] (*End of To do*) | "2" RIGHTA - [ ta0 = tactic_expr; "||"; ta1 = tactic_expr -> TacOrelse (ta0,ta1) ] + [ ta0 = tactic_expr; "||"; ta1 = binder_tactic -> TacOrelse (ta0,ta1) + | ta0 = tactic_expr; "||"; ta1 = tactic_expr -> TacOrelse (ta0,ta1) ] | "1" RIGHTA - [ "fun"; it = LIST1 input_fun ; "=>"; body = tactic_expr -> - TacFun (it,body) - | "let"; IDENT "rec"; rcl = LIST1 rec_clause SEP "with"; "in"; - body = tactic_expr -> TacLetRecIn (rcl,body) - | "let"; llc = LIST1 let_clause SEP "with"; "in"; - u = tactic_expr -> TacLetIn (make_letin_clause loc llc,u) - | b = match_key; IDENT "goal"; "with"; mrl = match_context_list; "end" -> + [ b = match_key; IDENT "goal"; "with"; mrl = match_context_list; "end" -> TacMatchContext (b,false,mrl) | b = match_key; IDENT "reverse"; IDENT "goal"; "with"; mrl = match_context_list; "end" -> @@ -104,6 +100,17 @@ GEXTEND Gram [ "("; a = tactic_expr; ")" -> a | a = tactic_atom -> TacArg a ] ] ; + (* binder_tactic: level 5 of tactic_expr *) + binder_tactic: + [ RIGHTA + [ "fun"; it = LIST1 input_fun ; "=>"; body = tactic_expr LEVEL "5" -> + TacFun (it,body) + | "let"; IDENT "rec"; rcl = LIST1 rec_clause SEP "with"; "in"; + body = tactic_expr LEVEL "5" -> TacLetRecIn (rcl,body) + | "let"; llc = LIST1 let_clause SEP "with"; "in"; + u = tactic_expr LEVEL "5" -> TacLetIn (make_letin_clause loc llc,u) + | IDENT "info"; tc = tactic_expr LEVEL "5" -> TacInfo tc ] ] + ; (* Tactic arguments *) tactic_arg: [ [ IDENT "ltac"; ":"; a = tactic_expr LEVEL "0" -> tacarg_of_expr a @@ -115,7 +122,10 @@ GEXTEND Gram ; may_eval_arg: [ [ c = constr_eval -> ConstrMayEval c - | IDENT "fresh"; s = OPT STRING -> TacFreshId s ] ] + | IDENT "fresh"; l = LIST0 fresh_id -> TacFreshId l ] ] + ; + fresh_id: + [ [ s = STRING -> ArgArg s | id = ident -> ArgVar (loc,id) ] ] ; constr_eval: [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr -> diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 94205fa8..2f515a81 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: g_proofs.ml4 8875 2006-05-29 19:59:11Z msozeau $ *) +(* $Id: g_proofs.ml4 9154 2006-09-20 17:18:18Z corbinea $ *) open Pcoq open Pp @@ -75,6 +75,7 @@ GEXTEND Gram | IDENT "Show"; IDENT "Intro" -> VernacShow (ShowIntros false) | IDENT "Show"; IDENT "Intros" -> VernacShow (ShowIntros true) | IDENT "Show"; IDENT "Match"; id = identref -> VernacShow (ShowMatch id) + | IDENT "Show"; IDENT "Thesis" -> VernacShow ShowThesis | IDENT "Explain"; IDENT "Proof"; l = LIST0 integer -> VernacShow (ExplainProof l) | IDENT "Explain"; IDENT "Proof"; IDENT "Tree"; l = LIST0 integer -> diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index a72ced97..9bbdc1d4 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 9017 2006-07-05 17:27:34Z herbelin $ *) +(* $Id: g_vernac.ml4 9306 2006-10-28 18:28:19Z herbelin $ *) (*i camlp4deps: "parsing/grammar.cma" i*) open Pp @@ -15,6 +15,7 @@ open Names open Topconstr open Vernacexpr open Pcoq +open Decl_mode open Tactic open Decl_kinds open Genarg @@ -34,13 +35,28 @@ let _ = List.iter (fun s -> Lexer.add_token ("",s)) vernac_kw (* compilation on PowerPC and Sun architectures *) let check_command = Gram.Entry.create "vernac:check_command" + +let tactic_mode = Gram.Entry.create "vernac:tactic_command" +let proof_mode = Gram.Entry.create "vernac:proof_command" +let noedit_mode = Gram.Entry.create "vernac:noedit_command" + let class_rawexpr = Gram.Entry.create "vernac:class_rawexpr" let thm_token = Gram.Entry.create "vernac:thm_token" let def_body = Gram.Entry.create "vernac:def_body" +let get_command_entry () = + match Decl_mode.get_current_mode () with + Mode_proof -> proof_mode + | Mode_tactic -> tactic_mode + | Mode_none -> noedit_mode + +let default_command_entry = + Gram.Entry.of_parser "command_entry" + (fun strm -> Gram.Entry.parse_token (get_command_entry ()) strm) + let no_hook _ _ = () GEXTEND Gram - GLOBAL: vernac gallina_ext; + GLOBAL: vernac gallina_ext tactic_mode proof_mode noedit_mode; vernac: (* Better to parse "." here: in case of failure (e.g. in coerce_to_var), *) (* "." is still in the stream and discard_to_dot works correctly *) @@ -54,9 +70,15 @@ GEXTEND Gram vernac: FIRST [ [ IDENT "Time"; v = vernac -> VernacTime v ] ] ; - vernac: LAST - [ [ gln = OPT[n=natural; ":" -> n]; - tac = subgoal_command -> tac gln ] ] + vernac: LAST + [ [ prfcom = default_command_entry -> prfcom ] ] + ; + noedit_mode: + [ [ c = subgoal_command -> c None] ] + ; + tactic_mode: + [ [ gln = OPT[n=natural; ":" -> n]; + tac = subgoal_command -> tac gln ] ] ; subgoal_command: [ [ c = check_command; "." -> c @@ -66,6 +88,12 @@ GEXTEND Gram let g = match g with Some gl -> gl | _ -> 1 in VernacSolve(g,tac,use_dft_tac)) ] ] ; + proof_mode: + [ [ instr = proof_instr; "." -> VernacProofInstr instr ] ] + ; + proof_mode: LAST + [ [ c=subgoal_command -> c (Some 1) ] ] + ; located_vernac: [ [ v = vernac -> loc, v ] ] ; @@ -191,9 +219,9 @@ GEXTEND Gram ; (* Inductives and records *) inductive_definition: - [ [ id = identref; indpar = LIST0 binder_let; ":"; c = lconstr; + [ [ id = identref; indpar = LIST0 binder_let; ":"; c = lconstr; ":="; lc = constructor_list; ntn = decl_notation -> - (id,ntn,indpar,c,lc) ] ] + ((id,indpar,c,lc),ntn) ] ] ; constructor_list: [ [ "|"; l = LIST1 constructor SEP "|" -> l @@ -212,7 +240,7 @@ GEXTEND Gram (* (co)-fixpoints *) rec_definition: [ [ id = ident; bl = LIST1 binder_let; - annot = rec_annotation; type_ = type_cstr; + annot = rec_annotation; ty = type_cstr; ":="; def = lconstr; ntn = decl_notation -> let names = List.map snd (names_of_local_assums bl) in let ni = @@ -227,12 +255,12 @@ GEXTEND Gram otherwise, we search the recursive index later *) if List.length names = 1 then Some 0 else None in - ((id, (ni, snd annot), bl, type_, def),ntn) ] ] + ((id,(ni,snd annot),bl,ty,def),ntn) ] ] ; corec_definition: - [ [ id = ident; bl = LIST0 binder_let; c = type_cstr; ":="; - def = lconstr -> - (id,bl,c ,def) ] ] + [ [ id = ident; bl = LIST0 binder_let; ty = type_cstr; ":="; + def = lconstr; ntn = decl_notation -> + ((id,bl,ty,def),ntn) ] ] ; rec_annotation: [ [ "{"; IDENT "struct"; id=IDENT; "}" -> (Some (id_of_string id), CStructRec) @@ -460,9 +488,8 @@ GEXTEND Gram | IDENT "Declare"; IDENT "ML"; IDENT "Module"; l = LIST1 ne_string -> VernacDeclareMLModule l - (* Dump of the universe graph - to file or to stdout *) | IDENT "Dump"; IDENT "Universes"; fopt = OPT ne_string -> - VernacPrint (PrintUniverses fopt) + error "This command is deprecated, use Print Universes" | IDENT "Locate"; l = locatable -> VernacLocate l @@ -556,7 +583,9 @@ GEXTEND Gram | IDENT "Remove"; table = IDENT; field = IDENT; v= LIST1 option_ref_value -> VernacRemoveOption (SecondaryTable (table,field), v) | IDENT "Remove"; table = IDENT; v = LIST1 option_ref_value -> - VernacRemoveOption (PrimaryTable table, v) ] ] + VernacRemoveOption (PrimaryTable table, v) + | IDENT "proof" -> VernacDeclProof + | "return" -> VernacReturn ]] ; check_command: (* TODO: rapprocher Eval et Check *) [ [ IDENT "Eval"; r = Tactic.red_expr; "in"; c = lconstr -> @@ -596,7 +625,8 @@ GEXTEND Gram | IDENT "Scopes" -> PrintScopes | IDENT "Scope"; s = IDENT -> PrintScope s | IDENT "Visibility"; s = OPT IDENT -> PrintVisibility s - | IDENT "Implicit"; qid = global -> PrintImplicit qid ] ] + | IDENT "Implicit"; qid = global -> PrintImplicit qid + | IDENT "Universes"; fopt = OPT ne_string -> PrintUniverses fopt ] ] ; class_rawexpr: [ [ IDENT "Funclass" -> FunClass diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index a89fffa0..c13532cc 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: g_xml.ml4 9016 2006-07-05 17:19:39Z herbelin $ *) +(* $Id: g_xml.ml4 9200 2006-10-03 14:11:08Z herbelin $ *) open Pp open Util @@ -146,9 +146,11 @@ let rec interp_xml_constr = function let ctx = List.map interp_xml_decl decls in List.fold_right (fun (na,t) b -> RProd (loc, na, t, b)) ctx (interp_xml_target body) - | XmlTag (loc,"LETIN",al,[x1;x2]) -> - let na,t = interp_xml_def x1 in - RLetIn (loc, na, t, interp_xml_target x2) + | XmlTag (loc,"LETIN",al,(_::_ as xl)) -> + let body,defs = list_sep_last xl in + let ctx = List.map interp_xml_def defs in + List.fold_right (fun (na,t) b -> RLetIn (loc, na, t, b)) + ctx (interp_xml_target body) | XmlTag (loc,"APPLY",_,x::xl) -> RApp (loc, interp_xml_constr x, List.map interp_xml_constr xl) | XmlTag (loc,"instantiate",_, diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 56e434fb..f7adfdd8 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pcoq.ml4 9043 2006-07-12 10:06:40Z herbelin $ i*) +(*i $Id: pcoq.ml4 9333 2006-11-02 13:59:14Z barras $ i*) open Pp open Util @@ -430,6 +430,7 @@ module Tactic = (* Main entries for ltac *) let tactic_arg = Gram.Entry.create "tactic:tactic_arg" let tactic_expr = Gram.Entry.create "tactic:tactic_expr" + let binder_tactic = Gram.Entry.create "tactic:binder_tactic" let tactic = make_gen_entry utactic (rawwit_tactic tactic_main_level) "tactic" @@ -451,6 +452,12 @@ module Vernac_ = let syntax = gec_vernac "syntax_command" let vernac = gec_vernac "Vernac_.vernac" + (* MMode *) + + let proof_instr = Gram.Entry.create "proofmode:instr" + + (* /MMode *) + let vernac_eoi = eoi_entry vernac end diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 3998d71b..1fe8c122 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pcoq.mli 8926 2006-06-08 20:23:17Z herbelin $ i*) +(*i $Id: pcoq.mli 9333 2006-11-02 13:59:14Z barras $ i*) open Util open Names @@ -184,6 +184,7 @@ module Tactic : val simple_intropattern : Genarg.intro_pattern_expr Gram.Entry.e val tactic_arg : raw_tactic_arg Gram.Entry.e val tactic_expr : raw_tactic_expr Gram.Entry.e + val binder_tactic : raw_tactic_expr Gram.Entry.e val tactic : raw_tactic_expr Gram.Entry.e val tactic_eoi : raw_tactic_expr Gram.Entry.e end @@ -196,6 +197,13 @@ module Vernac_ : val command : vernac_expr Gram.Entry.e val syntax : vernac_expr Gram.Entry.e val vernac : vernac_expr Gram.Entry.e + + (* MMode *) + + val proof_instr : Decl_expr.raw_proof_instr Gram.Entry.e + + (*/ MMode *) + val vernac_eoi : vernac_expr Gram.Entry.e end diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index a1ca386e..349d5df8 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ppconstr.ml 8997 2006-07-03 16:40:20Z herbelin $ *) +(* $Id: ppconstr.ml 9304 2006-10-28 09:58:16Z herbelin $ *) (*i*) open Util @@ -95,8 +95,6 @@ let pr_patnotation = pr_notation_gen decode_patlist_value let pr_delimiters key strm = strm ++ str ("%"^key) -let surround p = hov 1 (str"(" ++ p ++ str")") - let pr_located pr ((b,e),x) = if Options.do_translate() && (b,e)<>dummy_loc then let (b,e) = unloc (b,e) in @@ -115,12 +113,14 @@ let pr_optc pr = function | None -> mt () | Some x -> pr_sep_com spc pr x +let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)" + let pr_universe = Univ.pr_uni let pr_rawsort = function | RProp Term.Null -> str "Prop" | RProp Term.Pos -> str "Set" - | RType u -> str "Type" ++ pr_opt pr_universe u + | RType u -> hov 0 (str "Type" ++ pr_opt (pr_in_comment pr_universe) u) let pr_id = pr_id let pr_name = pr_name @@ -180,7 +180,7 @@ let rec pr_patt sep inh p = | CPatPrim (_,p) -> pr_prim_token p, latom | CPatDelimiters (_,k,p) -> pr_delimiters k (pr_patt mt lsimple p), 1 in - let loc = cases_pattern_loc p in + let loc = cases_pattern_expr_loc p in pr_with_comments loc (sep() ++ if prec_less prec inh then strm else surround strm) @@ -566,8 +566,9 @@ let rec pr sep inherited a = | CEvar (_,n) -> str (Evd.string_of_existential n), latom | CPatVar (_,(_,p)) -> str "?" ++ pr_patvar p, latom | CSort (_,s) -> pr_rawsort s, latom - | CCast (_,a,_,b) -> - hv 0 (pr mt (lcast,L) a ++ cut () ++ str ":" ++ pr mt (-lcast,E) b), + | CCast (_,a,k,b) -> + let s = match k with CastConv VMcast -> "<:" | _ -> ":" in + hv 0 (pr mt (lcast,L) a ++ cut () ++ str s ++ pr mt (-lcast,E) b), lcast | CNotation (_,"( _ )",[t]) -> pr (fun()->str"(") (max_int,L) t ++ str")", latom diff --git a/parsing/ppdecl_proof.ml b/parsing/ppdecl_proof.ml new file mode 100644 index 00000000..7e57885c --- /dev/null +++ b/parsing/ppdecl_proof.ml @@ -0,0 +1,180 @@ +(************************************************************************) +(* 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) -> + 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 + +let pr_statement pr_it env st = + pr_label st.st_label ++ pr_it env st.st_it + +let pr_or_thesis pr_this env = function + Thesis Plain -> str "thesis" + | Thesis (For id) -> + str "thesis" ++ spc() ++ str "for" ++ spc () ++ pr_id id + | Thesis (Sub n) -> str "thesis[" ++ int n ++ str "]" + | 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 + +let type_or_thesis = function + Thesis _ -> Term.mkProp + | This c -> c + +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 + match hyps with + (Hvar _ ::_) as rest -> + spc () ++ _andp ++ str "we have" ++ + print_vars pconstr gtyp env false _be 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 + end + | [] -> mt () + +and print_vars pconstr gtyp env _and _be vars = + match vars with + Hvar st :: rest -> + begin + let nenv = + 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 ++ + pr_statement pr_constr env st ++ + print_vars pconstr gtyp nenv true _be 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 + | [] -> mt () + +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 + +let pr_side = function + Lhs -> str "=~" + | Rhs -> str "~=" + +let rec pr_bare_proof_instr _then _thus env = function + | Pescape -> str "escape" + | Pthen i -> pr_bare_proof_instr true _thus env i + | Pthus i -> pr_bare_proof_instr _then true env i + | Phence i -> pr_bare_proof_instr true true env i + | Pcut c -> + begin + match _then,_thus with + false,false -> str "have" ++ spc () ++ + pr_cut (pr_or_thesis pr_constr) env c + | false,true -> str "thus" ++ spc () ++ + pr_cut (pr_or_thesis pr_constr) env c + | true,false -> str "then" ++ spc () ++ + pr_cut (pr_or_thesis pr_constr) env c + | true,true -> str "hence" ++ spc () ++ + pr_cut (pr_or_thesis pr_constr) env c + end + | Prew (sid,c) -> + (if _thus then str "thus" else str " ") ++ spc () ++ + pr_side sid ++ spc () ++ pr_cut pr_constr env c + | Passume hyps -> + str "assume" ++ print_hyps pr_constr _I env false false hyps + | Plet hyps -> + str "let" ++ print_vars pr_constr _I env false true 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 + ++ spc () ++ str "from " ++ pr_constr env id + | Pgiven hyps -> + str "given" ++ print_vars pr_constr _I env false false hyps + | Ptake witl -> + str "take" ++ spc () ++ + prlist_with_sep pr_coma (pr_constr env) witl + | Pdefine (id,args,body) -> + str "define" ++ spc () ++ pr_id id ++ spc () ++ + prlist_with_sep spc + (fun st -> str "(" ++ + pr_statement pr_constr env st ++ str ")") args ++ spc () ++ + str "as" ++ (pr_constr env body) + | Pcast (id,typ) -> + str "reconsider" ++ spc () ++ + pr_or_thesis (fun _ -> pr_id) env id ++ spc () ++ + str "as" ++ (pr_constr env typ) + | Psuppose hyps -> + str "suppose" ++ + print_hyps pr_constr _I env false false hyps + | Pcase (params,pat,hyps) -> + str "suppose it is" ++ spc () ++ pr_pat pat ++ + (if params = [] then mt () else + (spc () ++ str "with" ++ spc () ++ + prlist_with_sep spc + (fun st -> str "(" ++ + pr_statement pr_constr env st ++ str ")") params ++ spc ())) + ++ + (if hyps = [] then mt () else + (spc () ++ str "and" ++ + print_hyps (pr_or_thesis pr_constr) type_or_thesis + env false false hyps)) + | Pper (et,c) -> + str "per" ++ spc () ++ pr_elim_type et ++ spc () ++ + pr_casee env c + | Pend (B_elim et) -> str "end" ++ spc () ++ pr_elim_type et + | _ -> anomaly "unprintable instruction" + +let pr_emph = function + 0 -> str " " + | 1 -> str "* " + | 2 -> str "** " + | 3 -> str "*** " + | _ -> anomaly "unknown emphasis" + +let pr_proof_instr env instr = + pr_emph instr.emph ++ spc () ++ + pr_bare_proof_instr false false env instr.instr + diff --git a/parsing/ppdecl_proof.mli b/parsing/ppdecl_proof.mli new file mode 100644 index 00000000..b0f0e110 --- /dev/null +++ b/parsing/ppdecl_proof.mli @@ -0,0 +1,2 @@ + +val pr_proof_instr : Environ.env -> Decl_expr.proof_instr -> Pp.std_ppcmds diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 2113ae89..c7e1db60 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pptactic.ml 8926 2006-06-08 20:23:17Z herbelin $ *) +(* $Id: pptactic.ml 9319 2006-10-30 12:41:21Z barras $ *) open Pp open Names @@ -127,6 +127,8 @@ let rec pr_message_token prid = function | MsgInt n -> int n | MsgIdent id -> prid id +let pr_fresh_ids = prlist (fun s -> spc() ++ pr_or_var qs s) + let rec pr_raw_generic prc prlc prtac prref (x:(Genarg.rlevel, Tacexpr.raw_tactic_expr) Genarg.generic_argument) = match Genarg.genarg_tag x with | BoolArgType -> pr_arg str (if out_gen rawwit_bool x then "true" else "false") @@ -261,8 +263,6 @@ let rec pr_tacarg_using_rule pr_gen = function | [], [] -> mt () | _ -> failwith "Inconsistent arguments of extended tactic" -let surround p = hov 1 (str"(" ++ p ++ str")") - let pr_extend_gen prgen lev s l = try let tags = List.map genarg_tag l in @@ -521,11 +521,11 @@ let rec pr_tacarg_using_rule pr_gen = function let pr_then () = str ";" let ltop = (5,E) -let lseq = 5 +let lseq = 4 let ltactical = 3 let lorelse = 2 -let llet = 1 -let lfun = 1 +let llet = 5 +let lfun = 5 let lcomplete = 1 let labstract = 3 let lmatch = 1 @@ -533,6 +533,7 @@ let latom = 0 let lcall = 1 let leval = 1 let ltatom = 1 +let linfo = 5 let level_of (n,p) = match p with E -> n | L -> n-1 | Prec n -> n | Any -> lseq @@ -875,7 +876,7 @@ let rec pr_tac inherited tac = ltactical | TacInfo t -> hov 1 (str "info" ++ spc () ++ pr_tac (ltactical,E) t), - ltactical + linfo | TacOrelse (t1,t2) -> hov 1 (pr_tac (lorelse,L) t1 ++ str " ||" ++ brk (1,1) ++ pr_tac (lorelse,E) t2), @@ -902,7 +903,7 @@ let rec pr_tac inherited tac = str "constr:" ++ pr_constr c, latom | TacArg(ConstrMayEval c) -> pr_may_eval pr_constr pr_lconstr pr_cst c, leval - | TacArg(TacFreshId sopt) -> str "fresh" ++ pr_opt qs sopt, latom + | TacArg(TacFreshId l) -> str "fresh" ++ pr_fresh_ids l, latom | TacArg(Integer n) -> int n, latom | TacArg(TacCall(loc,f,l)) -> pr_with_comments loc @@ -923,7 +924,7 @@ and pr_tacarg = function | Reference r -> pr_ref r | ConstrMayEval c -> pr_may_eval pr_constr pr_lconstr pr_cst c - | TacFreshId sopt -> str "fresh" ++ pr_opt qs sopt + | TacFreshId l -> str "fresh" ++ pr_fresh_ids l | TacExternal (_,com,req,la) -> str "external" ++ spc() ++ qs com ++ spc() ++ qs req ++ spc() ++ prlist_with_sep spc pr_tacarg la diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 7e3c853d..f86b5708 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ppvernac.ml 9020 2006-07-05 17:35:23Z herbelin $ *) +(* $Id: ppvernac.ml 9154 2006-09-20 17:18:18Z corbinea $ *) open Pp open Names @@ -410,6 +410,7 @@ let rec pr_vernac = function | ShowProofNames -> str"Show Conjectures" | ShowIntros b -> str"Show " ++ (if b then str"Intros" else str"Intro") | ShowMatch id -> str"Show Match " ++ pr_lident id + | ShowThesis -> str "Show Thesis" | ExplainProof l -> str"Explain Proof" ++ spc() ++ prlist_with_sep sep int l | ExplainTree l -> str"Explain Proof Tree" ++ spc() ++ prlist_with_sep sep int l in pr_showable s @@ -530,7 +531,7 @@ let rec pr_vernac = function fnl() ++ str (if List.length l = 1 then " " else " | ") ++ prlist_with_sep (fun _ -> fnl() ++ str" | ") pr_constructor l in - let pr_oneind key (id,ntn,indpar,s,lc) = + let pr_oneind key ((id,indpar,s,lc),ntn) = hov 0 ( str key ++ spc() ++ pr_lident id ++ pr_and_type_binders_arg indpar ++ spc() ++ str":" ++ @@ -585,14 +586,16 @@ let rec pr_vernac = function prlist_with_sep (fun _ -> fnl() ++ fnl() ++ str"with ") pr_onerec recs) | VernacCoFixpoint (corecs,b) -> - let pr_onecorec (id,bl,c,def) = + let pr_onecorec ((id,bl,c,def),ntn) = let (bl',def,c) = if Options.do_translate() then extract_def_binders def c else ([],def,c) in let bl = bl @ bl' in pr_id id ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++ spc() ++ pr_lconstr_expr c ++ - str" :=" ++ brk(1,1) ++ pr_lconstr def in + str" :=" ++ brk(1,1) ++ pr_lconstr def ++ + pr_decl_notation pr_constr ntn + in let start = if b then "Boxed CoFixpoint" else "CoFixpoint" in hov 1 (str start ++ spc() ++ prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onecorec corecs) @@ -679,6 +682,14 @@ let rec pr_vernac = function | VernacSolveExistential (i,c) -> str"Existential " ++ int i ++ pr_lconstrarg c + (* MMode *) + + | VernacProofInstr instr -> anomaly "Not implemented" + | VernacDeclProof -> str "proof" + | VernacReturn -> str "return" + + (* /MMode *) + (* Auxiliary file and library management *) | VernacRequireFrom (exp,spe,f) -> hov 2 (str"Require" ++ spc() ++ pr_require_token exp ++ @@ -820,7 +831,7 @@ let rec pr_vernac = function (* For extension *) | VernacExtend (s,c) -> pr_extend s c - | VernacProof Tacexpr.TacId _ -> str "Proof" + | VernacProof (Tacexpr.TacId _) -> str "Proof" | VernacProof te -> str "Proof with" ++ spc() ++ pr_raw_tactic te and pr_extend s cl = diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 4534369f..57028469 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: prettyp.ml 8845 2006-05-23 07:41:58Z herbelin $ *) +(* $Id: prettyp.ml 9314 2006-10-29 20:11:08Z herbelin $ *) open Pp open Util @@ -246,6 +246,7 @@ let print_safe_judgment env j = let print_named_def name body typ = let pbody = pr_lconstr body in let ptyp = pr_ltype typ in + let pbody = if isCast body then surround pbody else pbody in (str "*** [" ++ str name ++ str " " ++ hov 0 (str ":=" ++ brk (1,2) ++ pbody ++ spc () ++ str ":" ++ brk (1,2) ++ ptyp) ++ @@ -278,11 +279,15 @@ let print_constructors envpar names types = hv 0 (str " " ++ pc) let build_inductive sp tyi = - let (mib,mip as specif) = Global.lookup_inductive (sp,tyi) in + let (mib,mip) = Global.lookup_inductive (sp,tyi) in let params = mib.mind_params_ctxt in let args = extended_rel_list 0 params in let env = Global.env() in - let arity = hnf_prod_applist env (Inductive.type_of_inductive specif) args in + let fullarity = match mip.mind_arity with + | Monomorphic ar -> ar.mind_user_arity + | Polymorphic ar -> + it_mkProd_or_LetIn (mkSort (Type ar.poly_level)) mip.mind_arity_ctxt in + let arity = hnf_prod_applist env fullarity args in let cstrtypes = arities_of_constructors env (sp,tyi) in let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in @@ -325,10 +330,14 @@ let print_body = function let print_typed_body (val_0,typ) = (print_body val_0 ++ fnl () ++ str " : " ++ pr_ltype typ ++ fnl ()) +let ungeneralized_type_of_constant_type = function + | PolymorphicArity (ctx,a) -> mkArity (ctx, Type a.poly_level) + | NonPolymorphicType t -> t + let print_constant with_values sep sp = let cb = Global.lookup_constant sp in let val_0 = cb.const_body in - let typ = cb.const_type in + let typ = ungeneralized_type_of_constant_type cb.const_type in hov 0 ( match val_0 with | None -> diff --git a/parsing/printer.ml b/parsing/printer.ml index 8cb5ac42..c0a98809 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: printer.ml 8831 2006-05-19 09:29:54Z herbelin $ *) +(* $Id: printer.ml 9164 2006-09-23 09:36:05Z herbelin $ *) open Pp open Util @@ -23,6 +23,7 @@ open Nametab open Ppconstr open Evd open Proof_type +open Decl_mode open Refiner open Pfedit open Ppconstr @@ -108,6 +109,13 @@ let pr_evaluable_reference ref = | EvalVarRef sp -> VarRef sp in pr_global ref' +(*let pr_rawterm t = + pr_lconstr (Constrextern.extern_rawconstr Idset.empty t)*) + +(*open Pattern + +let pr_pattern t = pr_pattern_env (Global.env()) empty_names_context t*) + (**********************************************************************) (* Contexts and declarations *) @@ -117,6 +125,7 @@ let pr_var_decl env (id,c,typ) = | Some c -> (* Force evaluation *) let pb = pr_lconstr_env env c in + let pb = if isCast c then surround pb else pb in (str" := " ++ pb ++ cut () ) in let pt = pr_ltype_env env typ in let ptyp = (str" : " ++ pt) in @@ -128,6 +137,7 @@ let pr_rel_decl env (na,c,typ) = | Some c -> (* Force evaluation *) let pb = pr_lconstr_env env c in + let pb = if isCast c then surround pb else pb in (str":=" ++ spc () ++ pb ++ spc ()) in let ptyp = pr_ltype_env env typ in match na with @@ -219,23 +229,53 @@ let pr_context_of env = match Options.print_hyps_limit () with | None -> hv 0 (pr_context_unlimited env) | Some n -> hv 0 (pr_context_limit n env) +(* 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 + hv 0 (prlist_with_sep mt pr_one metas) (* display complete goal *) let pr_goal g = let env = evar_env g in - let penv = pr_context_of env in - let pc = pr_ltype_env_at_top env g.evar_concl in - str" " ++ hv 0 (penv ++ fnl () ++ - str (emacs_str (String.make 1 (Char.chr 253))) ++ - str "============================" ++ fnl () ++ - str" " ++ pc) ++ fnl () - + let preamb,penv,pc = + if g.evar_extra = None then + mt (), + 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 + (str " *** Declarative Mode ***" ++ fnl ()++fnl ()), + pr_restricted_named_context among env, + pr_subgoal_metas metas env + in + preamb ++ + str" " ++ hv 0 (penv ++ fnl () ++ + str (emacs_str (String.make 1 (Char.chr 253))) ++ + str "============================" ++ fnl () ++ + str" " ++ pc) ++ fnl () + (* display the conclusion of a goal *) 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 "subgoal " ++ int n ++ str " is:" ++ cut () ++ str" " ++ pc + str (emacs_str (String.make 1 (Char.chr 253))) ++ + str "subgoal " ++ int n ++ str " is:" ++ cut () ++ str" " ++ pc + (* display evar type: a context and a type *) let pr_evgl_sign gl = @@ -266,15 +306,22 @@ let pr_subgoal n = prrec n (* Print open subgoals. Checks for uninstantiated existential variables *) -let pr_subgoals sigma = function +let pr_subgoals close_cmd sigma = function | [] -> - let exl = Evarutil.non_instantiated sigma in - if exl = [] then - (str"Proof completed." ++ fnl ()) - else - let pei = pr_evars_int 1 exl in - (str "No more subgoals but non-instantiated existential " ++ - str "variables :" ++fnl () ++ (hov 0 pei)) + begin + match close_cmd with + Some cmd -> + (str "Subproof completed, now type " ++ str cmd ++ + str "." ++ fnl ()) + | None -> + let exl = Evarutil.non_instantiated sigma in + if exl = [] then + (str"Proof completed." ++ fnl ()) + else + let pei = pr_evars_int 1 exl in + (str "No more subgoals but non-instantiated existential " ++ + str "variables :" ++fnl () ++ (hov 0 pei)) + end | [g] -> let pg = pr_goal g in v 0 (str ("1 "^"subgoal") ++cut () ++ pg) @@ -291,12 +338,12 @@ let pr_subgoals sigma = function v 0 (int(List.length rest+1) ++ str" subgoals" ++ cut () ++ pg1 ++ prest ++ fnl ()) - -let pr_subgoals_of_pfts pfts = +let pr_subgoals_of_pfts pfts = + let close_cmd = Decl_mode.get_end_command pfts in let gls = fst (Refiner.frontier (proof_of_pftreestate pfts)) in let sigma = (top_goal_of_pftreestate pfts).sigma in - pr_subgoals sigma gls - + pr_subgoals close_cmd sigma gls + let pr_open_subgoals () = let pfts = get_pftreestate () in match focus() with @@ -351,7 +398,6 @@ let pr_prim_rule = function (pr_id f ++ str" : " ++ pr_lconstr ar ++ print_mut oth) | [] -> mt () in (str"cofix " ++ pr_id f ++ str" with " ++ print_mut others) - | Refine c -> str(if occur_meta c then "refine " else "exact ") ++ Constrextern.with_meta_as_hole pr_constr c diff --git a/parsing/printer.mli b/parsing/printer.mli index 9d59bf75..6795889c 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 8831 2006-05-19 09:29:54Z herbelin $ i*) +(*i $Id: printer.mli 9249 2006-10-19 07:46:03Z herbelin $ i*) (*i*) open Pp @@ -35,6 +35,7 @@ val pr_lconstr : constr -> std_ppcmds val pr_constr_env : env -> constr -> std_ppcmds val pr_constr : constr -> std_ppcmds +val pr_ltype_env_at_top : env -> types -> std_ppcmds val pr_ltype_env : env -> types -> std_ppcmds val pr_ltype : types -> std_ppcmds @@ -87,7 +88,7 @@ val pr_context_of : env -> std_ppcmds (* Proofs *) val pr_goal : goal -> std_ppcmds -val pr_subgoals : evar_map -> goal list -> std_ppcmds +val pr_subgoals : string option -> evar_map -> goal list -> std_ppcmds val pr_subgoal : int -> goal list -> std_ppcmds val pr_open_subgoals : unit -> std_ppcmds diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index b5b07091..23d24497 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 8926 2006-06-08 20:23:17Z herbelin $ *) +(* $Id: q_coqast.ml4 9315 2006-10-29 21:53:30Z barras $ *) open Util open Names @@ -441,8 +441,12 @@ and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function $mlexpr_of_bool lz$ $mlexpr_of_bool lr$ $mlexpr_of_list (mlexpr_of_match_rule mlexpr_of_tactic) l$>> + + | Tacexpr.TacFun (idol,body) -> + <:expr< Tacexpr.TacFun + ($mlexpr_of_list mlexpr_of_ident_option idol$, + $mlexpr_of_tactic body$) >> (* - | Tacexpr.TacFun of $dloc$ * tactic_fun_ast | Tacexpr.TacFunRec of $dloc$ * identifier * tactic_fun_ast *) (* diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4 index 61a552f3..2ef56907 100644 --- a/parsing/q_util.ml4 +++ b/parsing/q_util.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: q_util.ml4 8982 2006-06-23 13:17:49Z herbelin $ *) +(* $Id: q_util.ml4 9333 2006-11-02 13:59:14Z barras $ *) (* This file defines standard combinators to build ml expressions *) @@ -71,22 +71,46 @@ open Vernacexpr open Pcoq open Genarg -let rec interp_entry_name loc s = +let modifiers e = +<:expr< Gramext.srules + [([], Gramext.action(fun _loc -> [])); + ([Gramext.Stoken ("", "("); + Gramext.Slist1sep ($e$, Gramext.Stoken ("", ",")); + Gramext.Stoken ("", ")")], + Gramext.action (fun _ l _ _loc -> l))] + >> + +let rec interp_entry_name loc s sep = let l = String.length s in if l > 8 & String.sub s 0 3 = "ne_" & String.sub s (l-5) 5 = "_list" then - let t, g = interp_entry_name loc (String.sub s 3 (l-8)) in + let t, g = interp_entry_name loc (String.sub s 3 (l-8)) "" in List1ArgType t, <:expr< Gramext.Slist1 $g$ >> + else if l > 12 & String.sub s 0 3 = "ne_" & + String.sub s (l-9) 9 = "_list_sep" then + let t, g = interp_entry_name loc (String.sub s 3 (l-12)) "" in + let sep = <:expr< Gramext.Stoken("",$str:sep$) >> in + List1ArgType t, <:expr< Gramext.Slist1sep $g$ $sep$ >> else if l > 5 & String.sub s (l-5) 5 = "_list" then - let t, g = interp_entry_name loc (String.sub s 0 (l-5)) in + let t, g = interp_entry_name loc (String.sub s 0 (l-5)) "" in List0ArgType t, <:expr< Gramext.Slist0 $g$ >> + else if l > 9 & String.sub s (l-9) 9 = "_list_sep" then + let t, g = interp_entry_name loc (String.sub s 0 (l-9)) "" in + let sep = <:expr< Gramext.Stoken("",$str:sep$) >> in + List0ArgType t, <:expr< Gramext.Slist0sep $g$ $sep$ >> else if l > 4 & String.sub s (l-4) 4 = "_opt" then - let t, g = interp_entry_name loc (String.sub s 0 (l-4)) in + let t, g = interp_entry_name loc (String.sub s 0 (l-4)) "" in OptArgType t, <:expr< Gramext.Sopt $g$ >> + else if l > 5 & String.sub s (l-5) 5 = "_mods" then + let t, g = interp_entry_name loc (String.sub s 0 (l-1)) "" in + List0ArgType t, modifiers g else let s = if s = "hyp" then "var" else s in let t, se, lev = match tactic_genarg_level s with - | Some n -> Some (ExtraArgType s), <:expr< Tactic. tactic_expr >>, Some n + | Some 5 -> + Some (ExtraArgType s), <:expr< Tactic. binder_tactic >>, None + | Some n -> + Some (ExtraArgType s), <:expr< Tactic. tactic_expr >>, Some n | None -> match Pcoq.entry_type (Pcoq.get_univ "prim") s with | Some _ as x -> x, <:expr< Prim. $lid:s$ >>, None diff --git a/parsing/q_util.mli b/parsing/q_util.mli index d31b217c..901f9198 100644 --- a/parsing/q_util.mli +++ b/parsing/q_util.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: q_util.mli 7732 2005-12-26 13:51:24Z herbelin $ i*) +(*i $Id: q_util.mli 9265 2006-10-24 08:35:38Z herbelin $ i*) val patt_of_expr : MLast.expr -> MLast.patt @@ -28,4 +28,5 @@ val mlexpr_of_string : string -> MLast.expr val mlexpr_of_option : ('a -> MLast.expr) -> 'a option -> MLast.expr -val interp_entry_name : Util.loc -> string -> Pcoq.entry_type * MLast.expr +val interp_entry_name : Util.loc -> string -> string -> + Pcoq.entry_type * MLast.expr diff --git a/parsing/search.ml b/parsing/search.ml index 995aa953..28362d72 100644 --- a/parsing/search.ml +++ b/parsing/search.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: search.ml 7837 2006-01-11 09:47:32Z herbelin $ *) +(* $Id: search.ml 9310 2006-10-28 19:35:09Z herbelin $ *) open Pp open Util @@ -57,12 +57,12 @@ let gen_crible refopt (fn : global_reference -> env -> constr -> unit) = fn (VarRef idc) env typ with Not_found -> (* we are in a section *) ()) | "CONSTANT" -> - let kn = locate_constant (qualid_of_sp sp) in - let {const_type=typ} = Global.lookup_constant kn in + let cst = locate_constant (qualid_of_sp sp) in + let typ = Typeops.type_of_constant env cst in if refopt = None || head_const typ = constr_of_global (out_some refopt) then - fn (ConstRef kn) env typ + fn (ConstRef cst) env typ | "INDUCTIVE" -> let kn = locate_mind (qualid_of_sp sp) in let mib = Global.lookup_mind kn in diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4 index 3d41e388..73d41465 100644 --- a/parsing/tacextend.ml4 +++ b/parsing/tacextend.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tacextend.ml4 8926 2006-06-08 20:23:17Z herbelin $ *) +(* $Id: tacextend.ml4 9265 2006-10-24 08:35:38Z herbelin $ *) open Genarg open Q_util @@ -165,7 +165,7 @@ let declare_tactic loc s cl = open Pcoq; declare $list:hidden$ end; try - let _=Refiner.add_tactic $se$ (fun [ $list:make_clauses s cl$ ]) in + let _=Tacinterp.add_tactic $se$ (fun [ $list:make_clauses s cl$ ]) in List.iter (fun s -> Tacinterp.add_primitive_tactic s (Tacexpr.TacAtom($default_loc$, @@ -198,7 +198,10 @@ EXTEND ; tacargs: [ [ e = LIDENT; "("; s = LIDENT; ")" -> - let t, g = Q_util.interp_entry_name loc e in + let t, g = Q_util.interp_entry_name loc e "" in + TacNonTerm (loc, t, g, Some s) + | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> + let t, g = Q_util.interp_entry_name loc e sep in TacNonTerm (loc, t, g, Some s) | s = STRING -> if s = "" then Util.user_err_loc (loc,"",Pp.str "Empty terminal"); diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml index 3584e375..6ea1c97e 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 7837 2006-01-11 09:47:32Z herbelin $ *) +(* $Id: tactic_printer.ml 9244 2006-10-16 17:11:44Z barras $ *) open Pp open Util @@ -15,6 +15,7 @@ open Evd open Tacexpr open Proof_type open Proof_trees +open Decl_expr open Logic open Printer @@ -25,19 +26,34 @@ let pr_tactic = function | t -> Pptactic.pr_tactic (Global.env()) t +let pr_proof_instr instr = + Ppdecl_proof.pr_proof_instr (Global.env()) instr + let pr_rule = function | Prim r -> hov 0 (pr_prim_rule r) - | Tactic (texp,_) -> hov 0 (pr_tactic texp) + | Nested(cmpd,_) -> + begin + match cmpd with + Tactic (texp,_) -> hov 0 (pr_tactic texp) + | Proof_instr (_,instr) -> hov 0 (pr_proof_instr instr) + 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 + | _ -> false + (* Does not print change of evars *) let pr_rule_dot = function | Change_evars -> mt () - | r -> pr_rule r ++ str"." + | r -> + pr_rule r ++ if uses_default_tac r then str "..." else str"." exception Different @@ -52,59 +68,145 @@ let thin_sign osign sign = sign ~init:Environ.empty_named_context_val let rec print_proof sigma osign pf = - let {evar_hyps=hyps; evar_concl=cl; - evar_body=body} = pf.goal in - let hyps = Environ.named_context_of_val hyps in + let hyps = Environ.named_context_of_val pf.goal.evar_hyps in let hyps' = thin_sign osign hyps in match pf.ref with | None -> - hov 0 (pr_goal {evar_hyps=hyps'; evar_concl=cl; evar_body=body}) + hov 0 (pr_goal {pf.goal with evar_hyps=hyps'}) | Some(r,spfl) -> hov 0 - (hov 0 (pr_goal {evar_hyps=hyps'; evar_concl=cl; evar_body=body}) ++ + (hov 0 (pr_goal {pf.goal with evar_hyps=hyps'}) ++ spc () ++ str" BY " ++ hov 0 (pr_rule r) ++ fnl () ++ str" " ++ - hov 0 (prlist_with_sep pr_fnl (print_proof sigma hyps) spfl) -) + hov 0 (prlist_with_sep pr_fnl (print_proof sigma hyps) spfl)) let pr_change gl = - str"Change " ++ + str"change " ++ pr_lconstr_env (Global.env_of_context gl.evar_hyps) gl.evar_concl ++ str"." -let rec print_script nochange sigma osign pf = - let {evar_hyps=sign; evar_concl=cl} = pf.goal in - let sign = Environ.named_context_of_val sign in +let rec print_decl_script tac_printer nochange sigma pf = + match pf.ref with + | None -> + (if nochange then + (str"") + else + pr_change pf.goal) + ++ fnl () + | Some (Daimon,_) -> mt () + | Some (Nested(Proof_instr (opened,instr),_) as rule,subprfs) -> + begin + match instr.instr,subprfs with + Pescape,[{ref=Some(_,subsubprfs)}] -> + hov 7 + (pr_rule_dot rule ++ fnl () ++ + prlist_with_sep pr_fnl tac_printer subsubprfs) ++ fnl () ++ + if opened then mt () else str "return." + | Pclaim _,[body;cont] -> + hov 2 + (pr_rule_dot rule ++ fnl () ++ + print_decl_script tac_printer nochange sigma body) ++ + fnl () ++ + if opened then mt () else str "end claim." ++ fnl () ++ + print_decl_script tac_printer nochange sigma cont + | Pfocus _,[body;cont] -> + hov 2 + (pr_rule_dot rule ++ fnl () ++ + print_decl_script tac_printer nochange sigma body) ++ + fnl () ++ + if opened then mt () else str "end focus." ++ fnl () ++ + print_decl_script tac_printer nochange sigma cont + | (Psuppose _ |Pcase (_,_,_)),[body;cont] -> + hov 2 + (pr_rule_dot rule ++ fnl () ++ + print_decl_script tac_printer nochange sigma body) ++ + fnl () ++ + print_decl_script tac_printer nochange sigma cont + | _,[next] -> + pr_rule_dot rule ++ fnl () ++ + print_decl_script tac_printer nochange sigma next + | _,[] -> + pr_rule_dot rule + | _,_ -> anomaly "unknown branching instruction" + end + | _ -> anomaly "Not Applicable" + +let rec print_script nochange sigma pf = match pf.ref with | None -> (if nochange then - (str"") - else - pr_change pf.goal) + (str"") + else + pr_change pf.goal) ++ fnl () - | Some(r,spfl) -> - ((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++ - pr_rule_dot r ++ fnl () ++ - prlist_with_sep pr_fnl - (print_script nochange sigma sign) spfl) + | Some(Decl_proof opened,script) -> + assert (List.length script = 1); + begin + if nochange then (mt ()) else (pr_change pf.goal ++ fnl ()) + end ++ + begin + hov 0 (str "proof." ++ fnl () ++ + print_decl_script (print_script nochange sigma) + nochange sigma (List.hd script)) + end ++ fnl () ++ + begin + if opened then mt () else (str "end proof." ++ fnl ()) + end + | Some(Daimon,spfl) -> + ((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++ + prlist_with_sep pr_fnl + (print_script nochange sigma) spfl ) + | Some(rule,spfl) -> + ((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++ + pr_rule_dot rule ++ fnl () ++ + prlist_with_sep pr_fnl + (print_script nochange sigma) spfl ) (* printed by Show Script command *) -let print_treescript nochange sigma _osign pf = + +let print_treescript nochange sigma pf = let rec aux top pf = match pf.ref with | None -> if nochange then - (str"") + if pf.goal.evar_extra=None then + (str"") + else (str"") else (pr_change pf.goal) + | Some(Decl_proof opened,script) -> + assert (List.length script = 1); + begin + if nochange then (mt ()) else (pr_change pf.goal ++ fnl ()) + end ++ + hov 0 + begin str "proof." ++ fnl () ++ + print_decl_script (aux false) + nochange sigma (List.hd script) + end ++ fnl () ++ + begin + if opened then mt () else (str "end proof." ++ fnl ()) + end + | Some(Daimon,spfl) -> + ((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++ + prlist_with_sep pr_fnl + (print_script nochange sigma) spfl ) | Some(r,spfl) -> (if nochange then mt () else (pr_change pf.goal ++ fnl ())) ++ - pr_rule_dot r ++ - match spfl with - | [] -> mt () - | [spf] -> fnl () ++ (if top then mt () else str " ") ++ aux top spf - | _ -> fnl () ++ str " " ++ - hov 0 (prlist_with_sep fnl (aux false) spfl) + pr_rule_dot r ++ + begin + if List.length spfl > 1 then + fnl () ++ + str " " ++ hov 0 (aux false (List.hd spfl)) ++ fnl () ++ + hov 0 (prlist_with_sep fnl (aux false) (List.tl spfl)) + else + match spfl with + | [] -> mt () + | [spf] -> fnl () ++ + (if top then mt () else str " ") ++ aux top spf + | _ -> fnl () ++ str " " ++ + hov 0 (prlist_with_sep fnl (aux false) spfl) + end in hov 0 (aux true pf) let rec print_info_script sigma osign pf = diff --git a/parsing/tactic_printer.mli b/parsing/tactic_printer.mli index db5dd794..b1f6d41c 100644 --- a/parsing/tactic_printer.mli +++ b/parsing/tactic_printer.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: tactic_printer.mli 6113 2004-09-17 20:28:19Z barras $ i*) +(*i $Id: tactic_printer.mli 9154 2006-09-20 17:18:18Z corbinea $ i*) (*i*) open Pp @@ -22,6 +22,6 @@ val print_proof : evar_map -> named_context -> proof_tree -> std_ppcmds val pr_rule : rule -> std_ppcmds val pr_tactic : tactic_expr -> std_ppcmds val print_script : - bool -> evar_map -> named_context -> proof_tree -> std_ppcmds + bool -> evar_map -> proof_tree -> std_ppcmds val print_treescript : - bool -> evar_map -> named_context -> proof_tree -> std_ppcmds + bool -> evar_map -> proof_tree -> std_ppcmds diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4 index af0d6781..7cf542fe 100644 --- a/parsing/vernacextend.ml4 +++ b/parsing/vernacextend.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: vernacextend.ml4 7732 2005-12-26 13:51:24Z herbelin $ *) +(* $Id: vernacextend.ml4 9265 2006-10-24 08:35:38Z herbelin $ *) open Genarg open Q_util @@ -114,7 +114,7 @@ EXTEND ; args: [ [ e = LIDENT; "("; s = LIDENT; ")" -> - let t, g = Q_util.interp_entry_name loc e in + let t, g = Q_util.interp_entry_name loc e "" in VernacNonTerm (loc, t, g, Some s) | s = STRING -> VernacTerm s -- cgit v1.2.3