diff options
| author |  Stephane Glondu <steph@glondu.net> | 2012-08-20 18:27:01 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2012-08-20 18:27:01 +0200 |
| commit | e0d682ec25282a348d35c5b169abafec48555690 (patch) | |
| tree | 1a46f0142a85df553388c932110793881f3af52f /parsing | |
| parent | 86535d84cc3cffeee1dcd8545343f234e7285530 (diff) | |
Imported Upstream version 8.4dfsgupstream/8.4dfsg
Diffstat (limited to 'parsing')
40 files changed, 244 insertions, 172 deletions
diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4 index f554522a..1888ef17 100644 --- a/parsing/argextend.ml4 +++ b/parsing/argextend.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index 82f24242..c68ba137 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli index 0ac46ded..f04809ce 100644 --- a/parsing/egrammar.mli +++ b/parsing/egrammar.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/parsing/extend.ml b/parsing/extend.ml index fca24ed5..0a76829b 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/parsing/extend.mli b/parsing/extend.mli index 6b29fc74..f63123cd 100644 --- a/parsing/extend.mli +++ b/parsing/extend.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/parsing/extrawit.ml b/parsing/extrawit.ml index 0398f0b6..75f6a7de 100644 --- a/parsing/extrawit.ml +++ b/parsing/extrawit.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/parsing/extrawit.mli b/parsing/extrawit.mli index 2d2eef37..8cd162c9 100644 --- a/parsing/extrawit.mli +++ b/parsing/extrawit.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 958f59e0..22dc427b 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index 2f129637..d082b91c 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -80,7 +80,6 @@ GEXTEND Gram TacFirst l | IDENT "solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" -> TacSolve l - | IDENT "complete" ; ta = tactic_expr -> TacComplete ta | IDENT "idtac"; l = LIST0 message_token -> TacId l | IDENT "fail"; n = [ n = int_or_var -> n | -> fail_default_value ]; l = LIST0 message_token -> TacFail (n,l) diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index 307e1779..6fee4e1f 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 23e7e31b..8a6f67c4 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 34590fb1..d265729a 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -130,21 +130,19 @@ let induction_arg_of_constr (c,lbind as clbind) = else ElimOnConstr clbind let mkTacCase with_evar = function - | [([ElimOnConstr cl],None,(None,None))],None -> + | [ElimOnConstr cl,(None,None)],None,None -> TacCase (with_evar,cl) (* Reinterpret numbers as a notation for terms *) - | [([(ElimOnAnonHyp n)],None,(None,None))],None -> + | [ElimOnAnonHyp n,(None,None)],None,None -> TacCase (with_evar, - (CPrim (dummy_loc, Numeral (Bigint.of_string (string_of_int n))), + (CPrim (dummy_loc, Numeral (Bigint.of_int n)), NoBindings)) (* Reinterpret ident as notations for variables in the context *) (* because we don't know if they are quantified or not *) - | [([ElimOnIdent id],None,(None,None))],None -> + | [ElimOnIdent id,(None,None)],None,None -> TacCase (with_evar,(CRef (Ident id),NoBindings)) | ic -> - if List.exists (fun (cl,a,b) -> - List.exists (function ElimOnAnonHyp _ -> true | _ -> false) cl) - (fst ic) + if List.exists (function (ElimOnAnonHyp _,_) -> true | _ -> false) (pi1 ic) then error "Use of numbers as direct arguments of 'case' is not supported."; TacInductionDestruct (false,with_evar,ic) @@ -279,11 +277,6 @@ GEXTEND Gram | "*" -> loc, IntroForthcoming true | "**" -> loc, IntroForthcoming false ] ] ; - intropattern_modifier: - [ [ IDENT "_eqn"; - id = [ ":"; id = naming_intropattern -> id | -> loc, IntroAnonymous ] - -> id ] ] - ; simple_intropattern: [ [ pat = disjunctive_intropattern -> pat | pat = naming_intropattern -> pat @@ -445,10 +438,15 @@ GEXTEND Gram [ [ "as"; ipat = simple_intropattern -> Some ipat | -> None ] ] ; - with_induction_names: - [ [ "as"; ipat = simple_intropattern; eq = OPT intropattern_modifier - -> (eq,Some ipat) - | -> (None,None) ] ] + eqn_ipat: + [ [ IDENT "eqn"; ":"; id = naming_intropattern -> Some id + | IDENT "_eqn"; ":"; id = naming_intropattern -> + let msg = "Obsolete syntax \"_eqn:H\" could be replaced by \"eqn:H\"" in + msg_warning (strbrk msg); Some id + | IDENT "_eqn" -> + let msg = "Obsolete syntax \"_eqn\" could be replaced by \"eqn:?\"" in + msg_warning (strbrk msg); Some (loc, IntroAnonymous) + | -> None ] ] ; as_name: [ [ "as"; id = ident -> Names.Name id | -> Names.Anonymous ] ] @@ -477,14 +475,11 @@ GEXTEND Gram [ [ b = orient; p = rewriter -> let (m,c) = p in (b,m,c) ] ] ; induction_clause: - [ [ lc = LIST1 induction_arg; ipats = with_induction_names; - el = OPT eliminator -> (lc,el,ipats) ] ] - ; - one_induction_clause: - [ [ ic = induction_clause; cl = opt_clause -> ([ic],cl) ] ] + [ [ c = induction_arg; pat = as_ipat; eq = eqn_ipat -> (c,(eq,pat)) ] ] ; induction_clause_list: - [ [ ic = LIST1 induction_clause SEP ","; cl = opt_clause -> (ic,cl) ] ] + [ [ ic = LIST1 induction_clause SEP ","; + el = OPT eliminator; cl = opt_clause -> (ic,el,cl) ] ] ; move_location: [ [ IDENT "after"; id = id_or_meta -> MoveAfter id @@ -535,15 +530,16 @@ GEXTEND Gram TacMutualCofix (false,id,List.map mk_cofix_tac fd) | IDENT "pose"; (id,b) = bindings_with_parameters -> - TacLetTac (Names.Name id,b,nowhere,true) + TacLetTac (Names.Name id,b,nowhere,true,None) | IDENT "pose"; b = constr; na = as_name -> - TacLetTac (na,b,nowhere,true) + TacLetTac (na,b,nowhere,true,None) | IDENT "set"; (id,c) = bindings_with_parameters; p = clause_dft_concl -> - TacLetTac (Names.Name id,c,p,true) + TacLetTac (Names.Name id,c,p,true,None) | IDENT "set"; c = constr; na = as_name; p = clause_dft_concl -> - TacLetTac (na,c,p,true) - | IDENT "remember"; c = constr; na = as_name; p = clause_dft_all -> - TacLetTac (na,c,p,false) + TacLetTac (na,c,p,true,None) + | IDENT "remember"; c = constr; na = as_name; e = eqn_ipat; + p = clause_dft_all -> + TacLetTac (na,c,p,false,e) (* Begin compatibility *) | IDENT "assert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":="; @@ -578,9 +574,9 @@ GEXTEND Gram (* Derived basic tactics *) | IDENT "simple"; IDENT"induction"; h = quantified_hypothesis -> TacSimpleInductionDestruct (true,h) - | IDENT "induction"; ic = one_induction_clause -> + | IDENT "induction"; ic = induction_clause_list -> TacInductionDestruct (true,false,ic) - | IDENT "einduction"; ic = one_induction_clause -> + | IDENT "einduction"; ic = induction_clause_list -> TacInductionDestruct(true,true,ic) | IDENT "double"; IDENT "induction"; h1 = quantified_hypothesis; h2 = quantified_hypothesis -> TacDoubleInduction (h1,h2) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 333934be..301370e7 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -927,8 +927,8 @@ GEXTEND Gram | IDENT "Restore"; IDENT "State"; s = ne_string -> VernacRestoreState s (* Resetting *) - | IDENT "Reset"; id = identref -> VernacResetName id | IDENT "Reset"; IDENT "Initial" -> VernacResetInitial + | IDENT "Reset"; id = identref -> VernacResetName id | IDENT "Back" -> VernacBack 1 | IDENT "Back"; n = natural -> VernacBack n | IDENT "BackTo"; n = natural -> VernacBackTo n @@ -976,8 +976,7 @@ GEXTEND Gram sc = OPT [ ":"; sc = IDENT -> sc ] -> VernacInfix (enforce_module_locality local,(op,modl),p,sc) | IDENT "Notation"; local = obsolete_locality; id = identref; - idl = LIST0 ident; ":="; c = constr; - b = [ "("; IDENT "only"; IDENT "parsing"; ")" -> true | -> false ] -> + idl = LIST0 ident; ":="; c = constr; b = only_parsing -> VernacSyntacticDefinition (id,(idl,c),enforce_module_locality local,b) | IDENT "Notation"; local = obsolete_locality; s = ne_lstring; ":="; @@ -1005,6 +1004,13 @@ GEXTEND Gram to factorize with other "Print"-based vernac entries *) ] ] ; + only_parsing: + [ [ "("; IDENT "only"; IDENT "parsing"; ")" -> + Some Flags.Current + | "("; IDENT "compat"; s = STRING; ")" -> + Some (Coqinit.get_compat_version s) + | -> None ] ] + ; obsolete_locality: [ [ IDENT "Local" -> true | -> false ] ] ; @@ -1020,7 +1026,10 @@ GEXTEND Gram | IDENT "left"; IDENT "associativity" -> SetAssoc LeftA | IDENT "right"; IDENT "associativity" -> SetAssoc RightA | IDENT "no"; IDENT "associativity" -> SetAssoc NonA - | IDENT "only"; IDENT "parsing" -> SetOnlyParsing + | IDENT "only"; IDENT "parsing" -> + SetOnlyParsing Flags.Current + | IDENT "compat"; s = STRING -> + SetOnlyParsing (Coqinit.get_compat_version s) | IDENT "format"; s = [s = STRING -> (loc,s)] -> SetFormat s | x = IDENT; ","; l = LIST1 [id = IDENT -> id ] SEP ","; "at"; lev = level -> SetItemLevel (x::l,lev) diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index c9e135ed..9dd0e369 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index e351061d..caea30b2 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/parsing/lexer.mli b/parsing/lexer.mli index 1899f7f4..a0820f55 100644 --- a/parsing/lexer.mli +++ b/parsing/lexer.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 075440f1..7f11af93 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index bba0e560..53c317c0 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index fa075536..5405e523 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -40,7 +40,9 @@ let lposint = 0 let lnegint = 35 (* must be consistent with Notation "- x" *) let ltop = (200,E) let lproj = 1 -let lsimple = (1,E) +let ldelim = 1 +let lsimpleconstr = (8,E) +let lsimplepatt = (1,E) let prec_less child (parent,assoc) = if parent < 0 && child = lprod then true @@ -149,7 +151,7 @@ let pr_or_var pr = function | ArgVar (loc,s) -> pr_lident (loc,s) let pr_prim_token = function - | Numeral n -> Bigint.pr_bigint n + | Numeral n -> str (Bigint.to_string n) | String s -> qs s let pr_evar pr n l = @@ -188,7 +190,7 @@ let rec pr_patt sep inh p = | CPatNotation (_,s,(l,ll)) -> pr_notation (pr_patt mt) (fun _ _ _ -> mt()) s (l,ll,[]) | CPatPrim (_,p) -> pr_prim_token p, latom - | CPatDelimiters (_,k,p) -> pr_delimiters k (pr_patt mt lsimple p), 1 + | CPatDelimiters (_,k,p) -> pr_delimiters k (pr_patt mt lsimplepatt p), 1 in let loc = cases_pattern_expr_loc p in pr_with_comments loc @@ -351,7 +353,7 @@ let pr_guard_annot pr_aux bl (n,ro) = (match r with None -> mt() | Some r -> str" on " ++ pr_aux r) ++ str"}" let pr_fixdecl pr prd dangling_with_for ((_,id),ro,bl,t,c) = - let annot = pr_guard_annot (pr lsimple) bl ro in + let annot = pr_guard_annot (pr lsimpleconstr) bl ro in pr_recursive_decl pr prd dangling_with_for id bl annot t c let pr_cofixdecl pr prd dangling_with_for ((_,id),bl,t,c) = @@ -371,7 +373,7 @@ let pr_asin pr (na,indnalopt) = | None -> mt ()) ++ (match indnalopt with | None -> mt () - | Some t -> spc () ++ str "in " ++ pr lsimple t) + | Some t -> spc () ++ str "in " ++ pr lsimpleconstr t) let pr_case_item pr (tm,asin) = hov 0 (pr (lcast,E) tm ++ pr_asin pr asin) @@ -380,7 +382,7 @@ let pr_case_type pr po = match po with | None | Some (CHole _) -> mt() | Some p -> - spc() ++ hov 2 (str "return" ++ pr_sep_com spc (pr lsimple) p) + spc() ++ hov 2 (str "return" ++ pr_sep_com spc (pr lsimpleconstr) p) let pr_simple_return_type pr na po = (match na with @@ -390,7 +392,7 @@ let pr_simple_return_type pr na po = pr_case_type pr po let pr_proj pr pr_app a f l = - hov 0 (pr lsimple a ++ cut() ++ str ".(" ++ pr_app pr f l ++ str ")") + hov 0 (pr (lproj,E) a ++ cut() ++ str ".(" ++ pr_app pr f l ++ str ")") let pr_appexpl pr f l = hov 2 ( @@ -545,9 +547,9 @@ let pr pr sep inherited a = pr (fun()->str"(") (max_int,L) t ++ str")", latom | CNotation (_,s,env) -> pr_notation (pr mt) (pr_binders_gen (pr mt ltop)) s env - | CGeneralization (_,bk,ak,c) -> pr_generalization bk ak (pr mt lsimple c), latom + | CGeneralization (_,bk,ak,c) -> pr_generalization bk ak (pr mt ltop c), latom | CPrim (_,p) -> pr_prim_token p, prec_of_prim_token p - | CDelimiters (_,sc,a) -> pr_delimiters sc (pr mt lsimple a), 1 + | CDelimiters (_,sc,a) -> pr_delimiters sc (pr mt (ldelim,E) a), ldelim in let loc = constr_loc a in pr_with_comments loc @@ -565,10 +567,14 @@ let modular_constr_pr = pr let rec fix rf x =rf (fix rf) x let pr = fix modular_constr_pr mt +let pr_simpleconstr = function + | CAppExpl (_,(None,f),[]) -> str "@" ++ pr_reference f + | c -> pr lsimpleconstr c + let default_term_pr = { - pr_constr_expr = pr lsimple; + pr_constr_expr = pr_simpleconstr; pr_lconstr_expr = pr ltop; - pr_constr_pattern_expr = pr lsimple; + pr_constr_pattern_expr = pr_simpleconstr; pr_lconstr_pattern_expr = pr ltop } diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli index afcdad3e..7a24eb9f 100644 --- a/parsing/ppconstr.mli +++ b/parsing/ppconstr.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -82,8 +82,9 @@ val default_term_pr : term_pr (** The modular constr printer. [modular_constr_pr pr s p t] prints the head of the term [t] and calls [pr] on its subterms. - [s] is typically {!Pp.mt} and [p] is [lsimple] for "constr" printers and [ltop] - for "lconstr" printers (spiwack: we might need more specification here). + [s] is typically {!Pp.mt} and [p] is [lsimpleconstr] for "constr" printers + and [ltop] for "lconstr" printers (spiwack: we might need more + specification here). We can make a new modular constr printer by overriding certain branches, for instance if we want to build a printer which prints "Prop" as "Omega" instead we can proceed as follows: @@ -94,7 +95,7 @@ val default_term_pr : term_pr taking its fixpoint. *) type precedence -val lsimple : precedence +val lsimpleconstr : precedence val ltop : precedence val modular_constr_pr : ((unit->std_ppcmds) -> precedence -> constr_expr -> std_ppcmds) -> diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 6e13d4e9..3720eb20 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -338,11 +338,15 @@ let pr_bindings prlc prc = pr_bindings_gen false prlc prc let pr_with_bindings prlc prc (c,bl) = hov 1 (prc c ++ pr_bindings prlc prc bl) +let pr_as_ipat pat = str "as " ++ pr_intro_pattern pat +let pr_eqn_ipat pat = str "eqn:" ++ pr_intro_pattern pat + let pr_with_induction_names = function | None, None -> mt () - | eqpat, ipat -> - spc () ++ hov 1 (str "as" ++ pr_opt pr_intro_pattern eqpat ++ - pr_opt pr_intro_pattern ipat) + | Some eqpat, None -> spc () ++ hov 1 (pr_eqn_ipat eqpat) + | None, Some ipat -> spc () ++ hov 1 (pr_as_ipat ipat) + | Some eqpat, Some ipat -> + spc () ++ hov 1 (pr_as_ipat ipat ++ spc () ++ pr_eqn_ipat eqpat) let pr_as_intro_pattern ipat = spc () ++ hov 1 (str "as" ++ spc () ++ pr_intro_pattern ipat) @@ -693,12 +697,13 @@ and pr_atom1 = function | TacGeneralizeDep c -> hov 1 (str "generalize" ++ spc () ++ str "dependent" ++ pr_constrarg c) - | TacLetTac (na,c,cl,true) when cl = nowhere -> + | TacLetTac (na,c,cl,true,_) when cl = nowhere -> hov 1 (str "pose" ++ pr_pose pr_lconstr pr_constr na c) - | TacLetTac (na,c,cl,b) -> + | TacLetTac (na,c,cl,b,e) -> hov 1 ((if b then str "set" else str "remember") ++ (if b then pr_pose pr_lconstr else pr_pose_as_style) pr_constr na c ++ + pr_opt (fun p -> pr_eqn_ipat p ++ spc ()) e ++ pr_clauses (Some b) pr_ident cl) (* | TacInstantiate (n,c,ConclLocation ()) -> hov 1 (str "instantiate" ++ spc() ++ @@ -714,14 +719,14 @@ and pr_atom1 = function | TacSimpleInductionDestruct (isrec,h) -> hov 1 (str "simple " ++ str (if isrec then "induction" else "destruct") ++ pr_arg pr_quantified_hypothesis h) - | TacInductionDestruct (isrec,ev,(l,cl)) -> + | TacInductionDestruct (isrec,ev,(l,el,cl)) -> hov 1 (str (with_evars ev (if isrec then "induction" else "destruct")) ++ spc () ++ - prlist_with_sep pr_comma (fun (h,e,ids) -> - prlist_with_sep spc (pr_induction_arg pr_lconstr pr_constr) h ++ - pr_with_induction_names ids ++ - pr_opt pr_eliminator e) l ++ - pr_opt_no_spc (pr_clauses None pr_ident) cl) + prlist_with_sep pr_comma (fun (h,ids) -> + pr_induction_arg pr_lconstr pr_constr h ++ + pr_with_induction_names ids) l ++ + pr_opt pr_eliminator el ++ + pr_opt_no_spc (pr_clauses None pr_ident) cl) | TacDoubleInduction (h1,h2) -> hov 1 (str "double induction" ++ @@ -911,7 +916,7 @@ let rec pr_tac inherited tac = | TacSolve tl -> str "solve" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet | TacComplete t -> - str "complete" ++ spc () ++ pr_tac (lcomplete,E) t, lcomplete + pr_tac (lcomplete,E) t, lcomplete | TacId l -> str "idtac" ++ prlist (pr_arg (pr_message_token pr_ident)) l, latom | TacAtom (loc,TacAlias (_,s,l,_)) -> diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli index d85f1ec3..0f82071d 100644 --- a/parsing/pptactic.mli +++ b/parsing/pptactic.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index cf9d4a53..f2491293 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -58,7 +58,11 @@ let pr_module = Libnames.pr_reference let pr_import_module = Libnames.pr_reference -let sep_end () = str"." +let sep_end = function + | VernacBullet _ + | VernacSubproof None + | VernacEndSubproof -> str"" + | _ -> str"." (* Warning: [pr_raw_tactic] globalises and fails if globalisation fails *) @@ -372,7 +376,8 @@ let pr_syntax_modifier = function | SetAssoc RightA -> str"right associativity" | SetAssoc NonA -> str"no associativity" | SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_entry_type typ - | SetOnlyParsing -> str"only parsing" + | SetOnlyParsing Flags.Current -> str"only parsing" + | SetOnlyParsing v -> str("compat \"" ^ Flags.pr_version v ^ "\"") | SetFormat s -> str"format " ++ pr_located qs s let pr_syntax_modifiers = function @@ -478,7 +483,7 @@ let rec pr_vernac = function (* Control *) | VernacList l -> hov 2 (str"[" ++ spc() ++ - prlist (fun v -> pr_located pr_vernac v ++ sep_end () ++ fnl()) l + prlist (fun v -> pr_located pr_vernac v ++ sep_end (snd v) ++ fnl()) l ++ spc() ++ str"]") | VernacLoad (f,s) -> str"Load" ++ if f then (spc() ++ str"Verbose" ++ spc()) else spc() ++ qs s @@ -780,7 +785,8 @@ let rec pr_vernac = function hov 2 (pr_locality local ++ str"Notation " ++ pr_lident id ++ spc () ++ prlist (fun x -> spc() ++ pr_id x) ids ++ str":=" ++ pr_constrarg c ++ - pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else [])) + pr_syntax_modifiers + (match onlyparsing with None -> [] | Some v -> [SetOnlyParsing v])) | VernacDeclareImplicits (local,q,[]) -> hov 2 (pr_section_locality local ++ str"Implicit Arguments" ++ spc() ++ pr_smart_global q) @@ -860,8 +866,8 @@ let rec pr_vernac = function | Some r0 -> hov 2 (str"Eval" ++ spc() ++ pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) r0 ++ - spc() ++ str"in" ++ spc () ++ pr_constr c) - | None -> hov 2 (str"Check" ++ spc() ++ pr_constr c) + spc() ++ str"in" ++ spc () ++ pr_lconstr c) + | None -> hov 2 (str"Check" ++ spc() ++ pr_lconstr c) in (if io = None then mt() else int (Option.get io) ++ str ": ") ++ pr_mayeval r c @@ -970,4 +976,4 @@ and pr_extend s cl = in pr_vernac -let pr_vernac v = make_pr_vernac pr_constr_expr pr_lconstr_expr v ++ sep_end () +let pr_vernac v = make_pr_vernac pr_constr_expr pr_lconstr_expr v ++ sep_end v diff --git a/parsing/ppvernac.mli b/parsing/ppvernac.mli index 7801de6a..6d381c72 100644 --- a/parsing/ppvernac.mli +++ b/parsing/ppvernac.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -21,6 +21,4 @@ open Libnames open Ppextend open Topconstr -val sep_end : unit -> std_ppcmds - val pr_vernac : vernac_expr -> std_ppcmds diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index e30979bf..d3eb40d0 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -673,16 +673,20 @@ let print_opaque_name qid = let (_,c,ty) = lookup_named id env in print_named_decl (id,c,ty) -let print_about_any k = +let print_about_any loc k = match k with | Term ref -> + Dumpglob.add_glob loc ref; pr_infos_list - ([print_ref false ref; blankline] @ + (print_ref false ref :: blankline :: print_name_infos ref @ print_simpl_behaviour ref @ print_opacity ref @ [hov 0 (str "Expands to: " ++ pr_located_qualid k)]) | Syntactic kn -> + let () = match Syntax_def.search_syntactic_definition kn with + | [],Topconstr.ARef ref -> Dumpglob.add_glob loc ref + | _ -> () in v 0 ( print_syntactic_def kn ++ hov 0 (str "Expands to: " ++ pr_located_qualid k)) ++ fnl() @@ -691,11 +695,11 @@ let print_about_any k = let print_about = function | Genarg.ByNotation (loc,ntn,sc) -> - print_about_any + print_about_any loc (Term (Notation.interp_notation_as_global_reference loc (fun _ -> true) ntn sc)) | Genarg.AN ref -> - print_about_any (locate_any_name ref) + print_about_any (loc_of_reference ref) (locate_any_name ref) (* for debug *) let inspect depth = diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli index 6d9c6ecc..84de2074 100644 --- a/parsing/prettyp.mli +++ b/parsing/prettyp.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/parsing/printer.ml b/parsing/printer.ml index 5352e0b7..9f0cb00d 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -333,7 +333,7 @@ let default_pr_subgoal n sigma = let emacs_print_dependent_evars sigma seeds = let evars () = - let evars = Evarutil.evars_of_evars_in_types_of_list sigma seeds in + let evars = Evarutil.gather_dependent_evars sigma seeds in let evars = Intmap.fold begin fun e i s -> let e' = str (string_of_existential e) in @@ -353,8 +353,34 @@ let emacs_print_dependent_evars sigma seeds = (* Print open subgoals. Checks for uninstantiated existential variables *) (* spiwack: [seeds] is for printing dependent evars in emacs mode. *) -let default_pr_subgoals close_cmd sigma seeds = function - | [] -> +(* spiwack: [pr_first] is true when the first goal must be singled out + and printed in its entirety. *) +(* courtieu: in emacs mode, even less cases where the first goal is printed + in its entirety *) +let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds stack goals = + let rec print_stack a = function + | [] -> Pp.int a + | b::l -> Pp.int a ++ str"-" ++ print_stack b l + in + let print_unfocused a l = + str"unfocused: " ++ print_stack a l + in + let rec pr_rec n = function + | [] -> (mt ()) + | g::rest -> + let pc = pr_concl n sigma g in + let prest = pr_rec (n+1) rest in + (cut () ++ pc ++ prest) + in + let print_multiple_goals g l = + if pr_first then + default_pr_goal { it = g ; sigma = sigma } ++ + pr_rec 2 l + else + pr_rec 1 (g::l) + in + match goals,stack with + | [],_ -> begin match close_cmd with Some cmd -> @@ -362,36 +388,43 @@ let default_pr_subgoals close_cmd sigma seeds = function str "." ++ fnl ()) | None -> let exl = Evarutil.non_instantiated sigma in - if exl = [] then - (str"No more subgoals." ++ fnl () - ++ emacs_print_dependent_evars sigma seeds) - else - let pei = pr_evars_int 1 exl in - (str "No more subgoals but non-instantiated existential " ++ - str "variables:" ++ fnl () ++ (hov 0 pei) - ++ emacs_print_dependent_evars sigma seeds ++ fnl () ++ - str "You can use Grab Existential Variables.") + if exl = [] then + (str"No more subgoals." + ++ emacs_print_dependent_evars sigma seeds) + else + let pei = pr_evars_int 1 exl in + (str "No more subgoals but non-instantiated existential " ++ + str "variables:" ++ fnl () ++ (hov 0 pei) + ++ emacs_print_dependent_evars sigma seeds ++ fnl () ++ + str "You can use Grab Existential Variables.") end - | [g] -> + | [g],[] when not !Flags.print_emacs -> let pg = default_pr_goal { it = g ; sigma = sigma } in v 0 ( - str ("1 "^"subgoal") ++ pr_goal_tag g ++ cut () ++ pg + str "1 subgoal" ++ pr_goal_tag g ++ cut () ++ pg ++ emacs_print_dependent_evars sigma seeds ) - | g1::rest -> - let rec pr_rec n = function - | [] -> (mt ()) - | g::rest -> - let pc = pr_concl n sigma g in - let prest = pr_rec (n+1) rest in - (cut () ++ pc ++ prest) - in - let pg1 = default_pr_goal { it = g1 ; sigma = sigma } in - let prest = pr_rec 2 rest in + | [g],a::l when not !Flags.print_emacs -> + let pg = default_pr_goal { it = g ; sigma = sigma } in + v 0 ( + str "1 focused subgoal (" ++ print_unfocused a l ++ str")" ++ pr_goal_tag g ++ cut () ++ pg + ++ emacs_print_dependent_evars sigma seeds + ) + | g1::rest,[] -> + let goals = print_multiple_goals g1 rest in v 0 ( int(List.length rest+1) ++ str" subgoals" ++ str (emacs_str ", subgoal 1") ++ pr_goal_tag g1 ++ cut () - ++ pg1 ++ prest ++ fnl () + ++ goals + ++ emacs_print_dependent_evars sigma seeds + ) + | g1::rest,a::l -> + let goals = print_multiple_goals g1 rest in + v 0 ( + int(List.length rest+1) ++ str" focused subgoals (" ++ + print_unfocused a l ++ str")" ++ cut () ++ + str (emacs_str ", subgoal 1") ++ pr_goal_tag g1 ++ cut () + ++ goals ++ emacs_print_dependent_evars sigma seeds ) @@ -400,7 +433,7 @@ let default_pr_subgoals close_cmd sigma seeds = function type printer_pr = { - pr_subgoals : string option -> evar_map -> evar list -> goal list -> std_ppcmds; + pr_subgoals : ?pr_first:bool -> string option -> evar_map -> evar list -> int list -> goal list -> std_ppcmds; pr_subgoal : int -> evar_map -> goal list -> std_ppcmds; pr_goal : goal sigma -> std_ppcmds; } @@ -415,7 +448,7 @@ let printer_pr = ref default_printer_pr let set_printer_pr = (:=) printer_pr -let pr_subgoals x = !printer_pr.pr_subgoals x +let pr_subgoals ?pr_first x = !printer_pr.pr_subgoals ?pr_first x let pr_subgoal x = !printer_pr.pr_subgoal x let pr_goal x = !printer_pr.pr_goal x @@ -423,24 +456,26 @@ let pr_goal x = !printer_pr.pr_goal x (**********************************************************************) let pr_open_subgoals () = + (* spiwack: it shouldn't be the job of the printer to look up stuff + in the [evar_map], I did stuff that way because it was more + straightforward, but seriously, [Proof.proof] should return + [evar_info]-s instead. *) let p = Proof_global.give_me_the_proof () in - let { Evd.it = goals ; sigma = sigma } = Proof.V82.subgoals p in + let (goals , stack , sigma ) = Proof.proof p in + let stack = List.map (fun (l,r) -> List.length l + List.length r) stack in let seeds = Proof.V82.top_evars p in begin match goals with | [] -> let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in - begin match bgoals with - | [] -> pr_subgoals None sigma seeds goals - | _ -> pr_subgoals None bsigma seeds bgoals ++ fnl () ++ fnl () ++ - str"This subproof is complete, but there are still unfocused goals." ++ fnl () - (* spiwack: to stay compatible with the proof general and coqide, - I use print the message after the goal. It would be better to have - something like: - str"This subproof is complete, but there are still unfocused goals:" - ++ fnl () ++ fnl () ++ pr_subgoals None bsigma bgoals - instead. But it doesn't quite work. - *) - end - | _ -> pr_subgoals None sigma seeds goals + begin match bgoals with + | [] -> pr_subgoals None sigma seeds stack goals + | _ -> + (* emacs mode: xml-like flag for detecting information message *) + str (emacs_str "<infomsg>") ++ + str"This subproof is complete, but there are still unfocused goals." + ++ str (emacs_str "</infomsg>") + ++ fnl () ++ fnl () ++ pr_subgoals ~pr_first:false None bsigma seeds [] bgoals + end + | _ -> pr_subgoals None sigma seeds stack goals end let pr_nth_open_subgoal n = diff --git a/parsing/printer.mli b/parsing/printer.mli index bbc3a6ca..a034f0ed 100644 --- a/parsing/printer.mli +++ b/parsing/printer.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -103,7 +103,7 @@ val pr_transparent_state : transparent_state -> std_ppcmds (** Proofs *) val pr_goal : goal sigma -> std_ppcmds -val pr_subgoals : string option -> evar_map -> evar list -> goal list -> std_ppcmds +val pr_subgoals : ?pr_first:bool -> string option -> evar_map -> evar list -> int list -> goal list -> std_ppcmds val pr_subgoal : int -> evar_map -> goal list -> std_ppcmds val pr_concl : int -> evar_map -> goal -> std_ppcmds @@ -140,7 +140,7 @@ val pr_assumptionset : val pr_goal_by_id : string -> std_ppcmds type printer_pr = { - pr_subgoals : string option -> evar_map -> evar list -> goal list -> std_ppcmds; + pr_subgoals : ?pr_first:bool -> string option -> evar_map -> evar list -> int list -> goal list -> std_ppcmds; pr_subgoal : int -> evar_map -> goal list -> std_ppcmds; pr_goal : goal sigma -> std_ppcmds; };; diff --git a/parsing/printmod.ml b/parsing/printmod.ml index 9cf76585..b4a8fdfd 100644 --- a/parsing/printmod.ml +++ b/parsing/printmod.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -220,9 +220,9 @@ let rec printable_body dir = state after the printing *) let print_modexpr' env mp mexpr = - States.with_state_protection (print_modexpr env mp []) mexpr + States.with_state_protection (fun e -> eval_ppcmds (print_modexpr env mp [] e)) mexpr let print_modtype' env mp mty = - States.with_state_protection (print_modtype env mp []) mty + States.with_state_protection (fun e -> eval_ppcmds (print_modtype env mp [] e)) mty let print_module' env mp with_body mb = let name = print_modpath [] mp in diff --git a/parsing/printmod.mli b/parsing/printmod.mli index a45bdb98..17ad6b25 100644 --- a/parsing/printmod.mli +++ b/parsing/printmod.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4 index 60543269..dfe7d9c0 100644 --- a/parsing/q_constr.ml4 +++ b/parsing/q_constr.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 6e3b3f35..02311fe4 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -343,11 +343,13 @@ let rec mlexpr_of_atomic_tactic = function (mlexpr_of_pair mlexpr_of_occ_constr mlexpr_of_name) cl$ >> | Tacexpr.TacGeneralizeDep c -> <:expr< Tacexpr.TacGeneralizeDep $mlexpr_of_constr c$ >> - | Tacexpr.TacLetTac (na,c,cl,b) -> + | Tacexpr.TacLetTac (na,c,cl,b,e) -> let na = mlexpr_of_name na in let cl = mlexpr_of_clause_pattern cl in <:expr< Tacexpr.TacLetTac $na$ $mlexpr_of_constr c$ $cl$ - $mlexpr_of_bool b$ >> + $mlexpr_of_bool b$ + (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern) e) + >> (* Derived basic tactics *) | Tacexpr.TacSimpleInductionDestruct (isrec,h) -> @@ -355,13 +357,15 @@ let rec mlexpr_of_atomic_tactic = function $mlexpr_of_quantified_hypothesis h$ >> | Tacexpr.TacInductionDestruct (isrec,ev,l) -> <:expr< Tacexpr.TacInductionDestruct $mlexpr_of_bool isrec$ $mlexpr_of_bool ev$ - $mlexpr_of_pair (mlexpr_of_list (mlexpr_of_triple - (mlexpr_of_list mlexpr_of_induction_arg) - (mlexpr_of_option mlexpr_of_constr_with_binding) - (mlexpr_of_pair - (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern)) - (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern))))) - (mlexpr_of_option mlexpr_of_clause) l$ >> + $mlexpr_of_triple + (mlexpr_of_list + (mlexpr_of_pair + mlexpr_of_induction_arg + (mlexpr_of_pair + (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern)) + (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern))))) + (mlexpr_of_option mlexpr_of_constr_with_binding) + (mlexpr_of_option mlexpr_of_clause) l$ >> (* Context management *) | Tacexpr.TacClear (b,l) -> diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4 index 91ab29f1..7fe5a3c4 100644 --- a/parsing/q_util.ml4 +++ b/parsing/q_util.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/parsing/q_util.mli b/parsing/q_util.mli index 5d56c456..527cc6b2 100644 --- a/parsing/q_util.mli +++ b/parsing/q_util.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4 index 05fdba42..dbc06856 100644 --- a/parsing/tacextend.ml4 +++ b/parsing/tacextend.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -188,7 +188,11 @@ let declare_tactic loc s cl = Tacexpr.TacExtend($default_loc$,$se$,l))) | None -> () ]) $atomic_tactics$ - with e -> Pp.pp (Errors.print e); + with e -> + Pp.msg_warning + (Stream.iapp + (Pp.str ("Exception in tactic extend " ^ $se$ ^": ")) + (Errors.print e)); Egrammar.extend_tactic_grammar $se$ $gl$; List.iter Pptactic.declare_extra_tactic_pprule $pp$; } >> ]) diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml index 83dae3dc..eaab1445 100644 --- a/parsing/tactic_printer.ml +++ b/parsing/tactic_printer.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/parsing/tactic_printer.mli b/parsing/tactic_printer.mli index 5ea57910..1c045e62 100644 --- a/parsing/tactic_printer.mli +++ b/parsing/tactic_printer.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/parsing/tok.ml b/parsing/tok.ml index bd7645c2..cf24aa5f 100644 --- a/parsing/tok.ml +++ b/parsing/tok.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/parsing/tok.mli b/parsing/tok.mli index 9a1edec5..a1ecd2c6 100644 --- a/parsing/tok.mli +++ b/parsing/tok.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4 index 88a75079..4f39019f 100644 --- a/parsing/vernacextend.ml4 +++ b/parsing/vernacextend.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -49,13 +49,18 @@ let mlexpr_of_clause = (Option.List.cons (Option.map (fun a -> GramTerminal a) a) b)) let declare_command loc s nt cl = + let se = mlexpr_of_string s in let gl = mlexpr_of_clause cl in let funcl = make_fun_clauses loc s cl in declare_str_items loc [ <:str_item< do { - try Vernacinterp.vinterp_add $mlexpr_of_string s$ $funcl$ - with e -> Pp.pp (Errors.print e); - Egrammar.extend_vernac_command_grammar $mlexpr_of_string s$ $nt$ $gl$ + try Vernacinterp.vinterp_add $se$ $funcl$ + with e -> + Pp.msg_warning + (Stream.iapp + (Pp.str ("Exception in vernac extend " ^ $se$ ^": ")) + (Errors.print e)); + Egrammar.extend_vernac_command_grammar $se$ $nt$ $gl$ } >> ] open Pcaml |