From ec5455d7351c05a58ae99d5a300dc8576f8c9360 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Fri, 4 Dec 2015 18:39:47 +0100
Subject: Extraction: nicer implementation of Implicits

 Instead of the original hacks (embedding implicits in string msg in MLexn !)
 we now use a proper construction MLdummy (Kimplicit (r,i)) to replace the use
 of the i-th argument of constant or constructor r when this argument has been
 declared as implicit.

 A new option Set/Unset Extraction SafeImplicits controls what happens
 when some implicits still occur after an extraction : fail in safe mode,
 or otherwise produce some code nonetheless. This code is probably buggish
 if the implicits are actually used to do anything relevant (match, function
 call, etc), but it might also be fine if the implicits are just passed along.
 And anyway, this unsafe mode could help figure what's going on.

 Note: the MLdummy now expected a kill_reason, just as Tdummy.
 These kill_reason are now Ktype, Kprop (formerly Kother) and Kimplicit.

 Some minor refactoring on the fly.
---
 plugins/extraction/scheme.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/extraction/scheme.ml')

diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index cc8b6d8e79..4901cf1807 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -126,7 +126,7 @@ let rec pp_expr env args =
     | MLexn s ->
 	(* An [MLexn] may be applied, but I don't really care. *)
 	paren (str "error" ++ spc () ++ qs s)
-    | MLdummy ->
+    | MLdummy _ ->
 	str "__" (* An [MLdummy] may be applied, but I don't really care. *)
     | MLmagic a ->
 	pp_expr env args a
-- 
cgit v1.2.3


From 123cbdfef1733a1786109bd1b97ccfa3f62c0d1c Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Mon, 14 Dec 2015 00:33:29 +0100
Subject: Extraction: cleanup a hack (Pp.is_empty instead of Failure "empty
 phrase")

---
 plugins/extraction/scheme.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'plugins/extraction/scheme.ml')

diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index 4901cf1807..0b2a04d3f1 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -183,7 +183,8 @@ let pp_decl = function
       prvecti
 	(fun i r ->
 	  let void = is_inline_custom r ||
-	    (not (is_custom r) && match defs.(i) with MLexn "UNUSED" -> true | _ -> false)
+	    (not (is_custom r) &&
+             match defs.(i) with MLexn "UNUSED" -> true | _ -> false)
 	  in
 	  if void then mt ()
 	  else
-- 
cgit v1.2.3