aboutsummaryrefslogtreecommitdiff
path: root/printing
diff options
context:
space:
mode:
Diffstat (limited to 'printing')
-rw-r--r--printing/genprint.ml2
-rw-r--r--printing/genprint.mli2
-rw-r--r--printing/miscprint.ml2
-rw-r--r--printing/miscprint.mli2
-rw-r--r--printing/ppannotation.ml2
-rw-r--r--printing/ppannotation.mli2
-rw-r--r--printing/ppconstr.ml2
-rw-r--r--printing/ppconstr.mli2
-rw-r--r--printing/ppconstrsig.mli2
-rw-r--r--printing/pptactic.ml2
-rw-r--r--printing/pptactic.mli2
-rw-r--r--printing/pptacticsig.mli2
-rw-r--r--printing/pputils.ml2
-rw-r--r--printing/pputils.mli2
-rw-r--r--printing/ppvernac.ml7
-rw-r--r--printing/ppvernac.mli2
-rw-r--r--printing/ppvernacsig.mli2
-rw-r--r--printing/prettyp.ml6
-rw-r--r--printing/prettyp.mli2
-rw-r--r--printing/printer.ml23
-rw-r--r--printing/printer.mli2
-rw-r--r--printing/printmod.ml2
-rw-r--r--printing/printmod.mli2
-rw-r--r--printing/printmodsig.mli2
-rw-r--r--printing/richprinter.mli2
25 files changed, 39 insertions, 41 deletions
diff --git a/printing/genprint.ml b/printing/genprint.ml
index ade69ef831..d4f792b753 100644
--- a/printing/genprint.ml
+++ b/printing/genprint.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/printing/genprint.mli b/printing/genprint.mli
index 5b91d6d216..6e6626f2f6 100644
--- a/printing/genprint.mli
+++ b/printing/genprint.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/printing/miscprint.ml b/printing/miscprint.ml
index d09af6d2ac..22db3d0bf6 100644
--- a/printing/miscprint.ml
+++ b/printing/miscprint.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/printing/miscprint.mli b/printing/miscprint.mli
index 1d915ef8c5..fe8c779ff4 100644
--- a/printing/miscprint.mli
+++ b/printing/miscprint.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/printing/ppannotation.ml b/printing/ppannotation.ml
index 4f26b82424..df7f925b73 100644
--- a/printing/ppannotation.ml
+++ b/printing/ppannotation.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/printing/ppannotation.mli b/printing/ppannotation.mli
index bc345c347b..84724053ed 100644
--- a/printing/ppannotation.mli
+++ b/printing/ppannotation.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 663b8b8101..e21bfa007d 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index 6e8d3b04c4..0241633c61 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/printing/ppconstrsig.mli b/printing/ppconstrsig.mli
index b7eb9b1fff..c711dd8f7f 100644
--- a/printing/ppconstrsig.mli
+++ b/printing/ppconstrsig.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index bc559460e0..7e903d2d3d 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/printing/pptactic.mli b/printing/pptactic.mli
index fa91aefcf3..3134656145 100644
--- a/printing/pptactic.mli
+++ b/printing/pptactic.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli
index 166a6675c1..b2323acba1 100644
--- a/printing/pptacticsig.mli
+++ b/printing/pptacticsig.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/printing/pputils.ml b/printing/pputils.ml
index ee1a39efd3..906b463a85 100644
--- a/printing/pputils.ml
+++ b/printing/pputils.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/printing/pputils.mli b/printing/pputils.mli
index 7287748327..a0f2c77283 100644
--- a/printing/pputils.mli
+++ b/printing/pputils.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 72b9cafe3f..38add9d2c8 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -925,8 +925,9 @@ module Make
hov 1 (
(if abst then keyword "Declare" ++ spc () else mt ()) ++
keyword "Instance" ++
- (match snd instid with Name id -> spc () ++ pr_lident (fst instid, id) ++ spc () |
- Anonymous -> mt ()) ++
+ (match instid with
+ | (loc, Name id), l -> spc () ++ pr_plident ((loc, id),l) ++ spc ()
+ | (_, Anonymous), _ -> mt ()) ++
pr_and_type_binders_arg sup ++
str":" ++ spc () ++
pr_constr cl ++ pr_priority pri ++
diff --git a/printing/ppvernac.mli b/printing/ppvernac.mli
index f38848cdcf..d3d4a5ceb7 100644
--- a/printing/ppvernac.mli
+++ b/printing/ppvernac.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/printing/ppvernacsig.mli b/printing/ppvernacsig.mli
index cfcd49744e..5d1c89332c 100644
--- a/printing/ppvernacsig.mli
+++ b/printing/ppvernacsig.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 84649e6ebf..4d9d40ae08 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -215,8 +215,8 @@ let print_polymorphism ref =
let print_primitive_record recflag mipv = function
| Some (Some (_, ps,_)) ->
let eta = match recflag with
- | Decl_kinds.CoFinite -> mt ()
- | Decl_kinds.Finite | Decl_kinds.BiFinite -> str " and has eta conversion"
+ | Decl_kinds.CoFinite | Decl_kinds.Finite -> mt ()
+ | Decl_kinds.BiFinite -> str " and has eta conversion"
in
[pr_id mipv.(0).mind_typename ++ str" is primitive" ++ eta ++ str"."]
| _ -> []
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index 6216d4d531..6f3556adba 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/printing/printer.ml b/printing/printer.ml
index 2e112f9ace..8469490f05 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -30,7 +30,8 @@ let delayed_emacs_cmd s =
let get_current_context () =
try Pfedit.get_current_goal_context ()
with e when Logic.catchable_exception e ->
- (Evd.empty, Global.env())
+ let env = Global.env () in
+ (Evd.from_env env, env)
(**********************************************************************)
(** Terms *)
@@ -380,16 +381,12 @@ let pr_transparent_state (ids, csts) =
let default_pr_goal gs =
let (g,sigma) = Goal.V82.nf_evar (project gs) (sig_it gs) in
let env = Goal.V82.env sigma g in
- let preamb,thesis,penv,pc =
- mt (), mt (),
- pr_context_of env sigma,
- pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g)
- in
- preamb ++
- str" " ++ hv 0 (penv ++ fnl () ++
- str (emacs_str "") ++
- str "============================" ++ fnl () ++
- thesis ++ str " " ++ pc)
+ let concl = Goal.V82.concl sigma g in
+ let goal =
+ pr_context_of env sigma ++ cut () ++
+ str "============================" ++ cut () ++
+ pr_goal_concl_style_env env sigma concl in
+ str " " ++ v 0 goal
(* display a goal tag *)
let pr_goal_tag g =
@@ -400,7 +397,7 @@ let display_name = false
(* display a goal name *)
let pr_goal_name sigma g =
- if display_name then str " " ++ Pp.surround (pr_id (Evd.evar_ident g sigma))
+ if display_name then str " " ++ Pp.surround (pr_existential_key sigma g)
else mt ()
(* display the conclusion of a goal *)
diff --git a/printing/printer.mli b/printing/printer.mli
index 5c60b89366..3424c41dc7 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 1d275c1aa6..c154b0aaa0 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/printing/printmod.mli b/printing/printmod.mli
index bea4753451..7f7d343927 100644
--- a/printing/printmod.mli
+++ b/printing/printmod.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/printing/printmodsig.mli b/printing/printmodsig.mli
index 5d0d4ab0b4..f71fffdcec 100644
--- a/printing/printmodsig.mli
+++ b/printing/printmodsig.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/printing/richprinter.mli b/printing/richprinter.mli
index 41c313514b..261d22c4c3 100644
--- a/printing/richprinter.mli
+++ b/printing/richprinter.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 14:49:04 +0000