summaryrefslogtreecommitdiff
path: root/parsing
diff options
context:
space:
mode:
Diffstat (limited to 'parsing')
-rw-r--r--parsing/argextend.ml42
-rw-r--r--parsing/egrammar.ml2
-rw-r--r--parsing/egrammar.mli2
-rw-r--r--parsing/extend.ml2
-rw-r--r--parsing/extend.mli2
-rw-r--r--parsing/extrawit.ml2
-rw-r--r--parsing/extrawit.mli2
-rw-r--r--parsing/g_constr.ml42
-rw-r--r--parsing/g_ltac.ml43
-rw-r--r--parsing/g_prim.ml42
-rw-r--r--parsing/g_proofs.ml42
-rw-r--r--parsing/g_tactic.ml458
-rw-r--r--parsing/g_vernac.ml419
-rw-r--r--parsing/g_xml.ml42
-rw-r--r--parsing/lexer.ml42
-rw-r--r--parsing/lexer.mli2
-rw-r--r--parsing/pcoq.ml42
-rw-r--r--parsing/pcoq.mli2
-rw-r--r--parsing/ppconstr.ml30
-rw-r--r--parsing/ppconstr.mli9
-rw-r--r--parsing/pptactic.ml31
-rw-r--r--parsing/pptactic.mli2
-rw-r--r--parsing/ppvernac.ml22
-rw-r--r--parsing/ppvernac.mli4
-rw-r--r--parsing/prettyp.ml14
-rw-r--r--parsing/prettyp.mli2
-rw-r--r--parsing/printer.ml119
-rw-r--r--parsing/printer.mli6
-rw-r--r--parsing/printmod.ml6
-rw-r--r--parsing/printmod.mli2
-rw-r--r--parsing/q_constr.ml42
-rw-r--r--parsing/q_coqast.ml424
-rw-r--r--parsing/q_util.ml42
-rw-r--r--parsing/q_util.mli2
-rw-r--r--parsing/tacextend.ml48
-rw-r--r--parsing/tactic_printer.ml2
-rw-r--r--parsing/tactic_printer.mli2
-rw-r--r--parsing/tok.ml2
-rw-r--r--parsing/tok.mli2
-rw-r--r--parsing/vernacextend.ml413
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