From 24a125b779c0cf6e9b0662e122c74aa80eb1837b Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 3 May 2016 08:21:36 +0200
Subject: Remove extraneous space in coqtop/pg output (bug #4675).

---
 plugins/decl_mode/g_decl_mode.ml4 | 19 ++++++++-----------
 1 file changed, 8 insertions(+), 11 deletions(-)

(limited to 'plugins')

diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index b62cfd6add..4c5c65669a 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -24,17 +24,14 @@ open Ppdecl_proof
 let pr_goal gs =
   let (g,sigma) = Goal.V82.nf_evar (Tacmach.project gs) (Evd.sig_it gs) in
   let env = Goal.V82.env sigma g in
-  let preamb,thesis,penv,pc =
-    (str "     *** Declarative Mode ***" ++ fnl ()++fnl ()),
-    (str "thesis := "  ++ fnl ()),
-    Printer.pr_context_of env sigma,
-    Printer.pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g)
-  in
-    preamb ++
-    str"  " ++ hv 0 (penv ++ fnl () ++
-		       str (Printer.emacs_str "")  ++
-		       str "============================" ++ fnl ()  ++
-		       thesis ++ str " " ++  pc) ++ fnl ()
+  let concl = Goal.V82.concl sigma g in
+  let goal =
+    Printer.pr_context_of env sigma ++ cut () ++
+      str "============================" ++ cut ()  ++
+      str "thesis :=" ++ cut () ++
+      Printer.pr_goal_concl_style_env env sigma concl in
+  str "     *** Declarative Mode ***" ++ fnl () ++ fnl () ++
+    str "  " ++ v 0 goal
 
 let pr_subgoals ?(pr_first=true) _ sigma _ _ _ gll =
   match gll with
-- 
cgit v1.2.3


From dd7cf3a8086fa8a08a421314caec8543ba62226b Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 4 May 2016 10:36:43 +0200
Subject: Handle primitive projections inside types when extracting (bug
 #4616).

Note that extracting terms containing primitive projections is still
utterly broken, so don't use them.
---
 plugins/extraction/extraction.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 10644da25d..667721e670 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -285,7 +285,7 @@ let rec extract_type env db j c args =
     | Ind ((kn,i),u) ->
 	let s = (extract_ind env kn).ind_packets.(i).ip_sign in
 	extract_type_app env db (IndRef (kn,i),s) args
-    | Case _ | Fix _ | CoFix _ -> Tunknown
+    | Case _ | Fix _ | CoFix _ | Proj _ -> Tunknown
     | _ -> assert false
 
 (*s Auxiliary function dealing with type application.
-- 
cgit v1.2.3


From 78e616d56dc0646d0c67ab57e11671a6c08d0cc7 Mon Sep 17 00:00:00 2001
From: Nickolai Zeldovich
Date: Mon, 8 Feb 2016 16:08:10 -0500
Subject: Fix Haskell extraction for terms over 45 characters long

The Haskell extraction code would allow line-wrapping of the Haskell
type definition, which would lead to unparseable Haskell code when the
linebreak occured just before the type name.  In particular, with a term
name of 46 characters or more, the following Coq code:

  Definition xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx := tt.
  Extraction Language Haskell.
  Extraction xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx.

would produce:

  xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx ::
  Unit
  xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx =
    Tt

which failed to compile with GHC (according to Haskell's indentation
rules, the "Unit" line must be indented to be treated as a continuation
of the previous line).

This patch always forces the type onto a separate line, and ensures that
it is always indented by 2 spaces (just like the body of each definition).
---
 plugins/extraction/haskell.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 22519e3471..764223621e 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -346,7 +346,7 @@ let pp_decl = function
 	  in
 	  if void then mt ()
 	  else
-	    names.(i) ++ str " :: " ++ pp_type false [] typs.(i) ++ fnl () ++
+	    hov 2 (names.(i) ++ str " :: " ++ pp_type false [] typs.(i)) ++ fnl () ++
 	    (if is_custom r then
 		(names.(i) ++ str " = " ++ str (find_custom r))
 	     else
@@ -357,7 +357,7 @@ let pp_decl = function
       if is_inline_custom r then mt ()
       else
 	let e = pp_global Term r in
-	e ++ str " :: " ++ pp_type false [] t ++ fnl () ++
+	hov 2 (e ++ str " :: " ++ pp_type false [] t) ++ fnl () ++
 	  if is_custom r then
 	    hov 0 (e ++ str " = " ++ str (find_custom r) ++ fnl2 ())
 	  else
-- 
cgit v1.2.3