Merge branch 'v8.5' into trunk

21 files changed, 389 insertions, 29 deletions

diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml
index 07df7c7f09..774c20c9ae 100644
--- a/plugins/decl_mode/decl_mode.ml
+++ b/plugins/decl_mode/decl_mode.ml
@@ -119,3 +119,18 @@ let get_last env = match Environ.named_context env with
   | (id,_,_)::_ -> id
   | [] -> error "no previous statement to use"
 
+
+let get_end_command pts =
+  match get_top_stack pts with
+  | [] -> "\"end proof\""
+  | Claim::_ -> "\"end claim\""
+  | Focus_claim::_-> "\"end focus\""
+  | Suppose_case :: Per (et,_,_,_) :: _ | Per (et,_,_,_) :: _  ->
+      begin
+	match et with
+	  Decl_expr.ET_Case_analysis ->
+	    "\"end cases\" or start a new case"
+	| Decl_expr.ET_Induction ->
+	    "\"end induction\" or start a new case"
+      end
+  | _ -> anomaly (Pp.str"lonely suppose")
diff --git a/plugins/decl_mode/decl_mode.mli b/plugins/decl_mode/decl_mode.mli
index e12c4c9237..fd7e15c150 100644
--- a/plugins/decl_mode/decl_mode.mli
+++ b/plugins/decl_mode/decl_mode.mli
@@ -72,6 +72,8 @@ val get_last:  Environ.env -> Id.t
 (** [get_last] raises a [UserError] when it cannot find a previous
     statement in the environment. *)
 
+val get_end_command : Proof.proof -> string
+
 val focus : Proof.proof -> unit
 
 val unfocus : unit -> unit
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index ab5282e791..9d0b7f3466 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -1446,6 +1446,7 @@ let rec postprocess pts instr =
 		  anomaly (Pp.str "\"end induction\" generated an ill-formed fixpoint")
 	end
     | Pend (B_elim ET_Case_analysis) -> goto_current_focus ()
+    | Pend B_proof -> Proof_global.set_proof_mode "Classic"
     | Pend _ -> ()
 
 let do_instr raw_instr pts =
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 2bd88d5aea..d598e7c3fa 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -36,13 +36,20 @@ let pr_goal gs =
 		       str "============================" ++ fnl ()  ++
 		       thesis ++ str " " ++  pc) ++ fnl ()
 
-(* arnaud: rebrancher ça ?
-let pr_open_subgoals () =
-  let p = Proof_global.give_me_the_proof () in
-  let { Evd.it = goals ; sigma = sigma } = Proof.V82.subgoals p in
-  let close_cmd = Decl_mode.get_end_command p in
-  pr_subgoals close_cmd sigma goals
-*)
+let pr_subgoals ?(pr_first=true) _ sigma _ _ _ gll =
+  match gll with
+  | [goal] when pr_first ->
+      pr_goal { Evd.it = goal ; sigma = sigma }
+  | _ ->
+      (* spiwack: it's not very nice to have to call proof global
+         here, a more robust solution would be to add a hook for
+         [Printer.pr_open_subgoals] in proof modes, in order to
+         compute the end command. Yet a more robust solution would be
+         to have focuses give explanations of their unfocusing
+         behaviour. *)
+      let p = Proof_global.give_me_the_proof () in
+      let close_cmd = Decl_mode.get_end_command p in
+      str "Subproof completed, now type " ++ str close_cmd ++ str "."
 
 let interp_proof_instr _ { Evd.it = gl ; sigma = sigma }=
   Decl_interp.interp_proof_instr 
@@ -93,14 +100,16 @@ let proof_instr : raw_proof_instr Gram.entry =
 let _ = Pptactic.declare_extra_genarg_pprule wit_proof_instr
   pr_raw_proof_instr pr_glob_proof_instr pr_proof_instr
 
-let classify_proof_instr _ = VtProofStep false, VtLater
+let classify_proof_instr = function
+  | { instr = Pescape |Pend B_proof } -> VtProofMode "Classic", VtNow
+  | _ -> VtProofStep false, VtLater
 
 (* We use the VERNAC EXTEND facility with a custom non-terminal
     to populate [proof_mode] with a new toplevel interpreter.
     The "-" indicates that the rule does not start with a distinguished
     string. *)
-VERNAC proof_mode EXTEND ProofInstr CLASSIFIED BY classify_proof_instr
-  [ - proof_instr(instr) ] -> [ vernac_proof_instr instr ]
+VERNAC proof_mode EXTEND ProofInstr
+  [ - proof_instr(instr) ] => [classify_proof_instr instr] -> [ vernac_proof_instr instr ]
 END
 
 (* It is useful to use GEXTEND directly to call grammar entries that have been
@@ -130,7 +139,8 @@ let _ =
 					 (* We substitute the goal printer, by the one we built
 					     for the proof mode. *)
 					 Printer.set_printer_pr { Printer.default_printer_pr with
-								                Printer.pr_goal = pr_goal }
+								                Printer.pr_goal = pr_goal;
+                                                                                pr_subgoals = pr_subgoals; }
 				       end ;
                                        (* function [reset] goes back to No Proof Mode from
 					   Declarative Proof Mode *)
@@ -147,7 +157,7 @@ VERNAC COMMAND EXTEND DeclProof
 [ "proof" ] => [ VtProofMode "Declarative", VtNow ] -> [ vernac_decl_proof () ]
 END
 VERNAC COMMAND EXTEND  DeclReturn
-[ "return" ] => [ VtProofMode "Classic", VtNow ] -> [ vernac_return () ]
+[ "return" ] => [ VtProofMode "Declarative", VtNow ] -> [ vernac_return () ]
 END
 
 let none_is_empty = function
diff --git a/plugins/extraction/ExtrHaskellBasic.v b/plugins/extraction/ExtrHaskellBasic.v
new file mode 100644
index 0000000000..294d61023b
--- /dev/null
+++ b/plugins/extraction/ExtrHaskellBasic.v
@@ -0,0 +1,15 @@
+(** Extraction to Haskell : use of basic Haskell types *)
+
+Extract Inductive bool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].
+Extract Inductive option => "Prelude.Maybe" [ "Prelude.Just" "Prelude.Nothing" ].
+Extract Inductive unit => "()" [ "()" ].
+Extract Inductive list => "([])" [ "([])" "(:)" ].
+Extract Inductive prod => "(,)" [ "(,)" ].
+
+Extract Inductive sumbool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].
+Extract Inductive sumor => "Prelude.Maybe" [ "Prelude.Just" "Prelude.Nothing" ].
+Extract Inductive sum => "Prelude.Either" [ "Prelude.Left" "Prelude.Right" ].
+
+Extract Inlined Constant andb => "(Prelude.&&)".
+Extract Inlined Constant orb => "(Prelude.||)".
+Extract Inlined Constant negb => "Prelude.not".
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 21819aa8f1..97f856944c 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -600,6 +600,7 @@ let pp_global k r =
     let rls = List.rev ls in (* for what come next it's easier this way *)
     match lang () with
       | Scheme -> unquote s (* no modular Scheme extraction... *)
+      | JSON -> dottify (List.map unquote rls)
       | Haskell -> if modular () then pp_haskell_gen k mp rls else s
       | Ocaml -> pp_ocaml_gen k mp rls (Some l)
 
@@ -628,7 +629,7 @@ let check_extract_ascii () =
   try
     let char_type = match lang () with
       | Ocaml -> "char"
-      | Haskell -> "Char"
+      | Haskell -> "Prelude.Char"
       | _ -> raise Not_found
     in
     String.equal (find_custom (IndRef (ind_ascii, 0))) (char_type)
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 5ea4fb763e..0f846013b2 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -410,6 +410,7 @@ let descr () = match lang () with
   | Ocaml -> Ocaml.ocaml_descr
   | Haskell -> Haskell.haskell_descr
   | Scheme -> Scheme.scheme_descr
+  | JSON -> Json.json_descr
 
 (* From a filename string "foo.ml" or "foo", builds "foo.ml" and "foo.mli"
    Works similarly for the other languages. *)
diff --git a/plugins/extraction/extraction_plugin.mllib b/plugins/extraction/extraction_plugin.mllib
index b7f458611a..ad32124347 100644
--- a/plugins/extraction/extraction_plugin.mllib
+++ b/plugins/extraction/extraction_plugin.mllib
@@ -6,6 +6,7 @@ Common
 Ocaml
 Haskell
 Scheme
+Json
 Extract_env
 G_extraction
 Extraction_plugin_mod
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index 3caa558f9b..3fe5a8c04e 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -41,12 +41,14 @@ let pr_language = function
   | Ocaml -> str "Ocaml"
   | Haskell -> str "Haskell"
   | Scheme -> str "Scheme"
+  | JSON -> str "JSON"
 
 VERNAC ARGUMENT EXTEND language
 PRINTED BY pr_language
 | [ "Ocaml" ] -> [ Ocaml ]
 | [ "Haskell" ] -> [ Haskell ]
 | [ "Scheme" ] -> [ Scheme ]
+| [ "JSON" ] -> [ JSON ]
 END
 
 (* Extraction commands *)
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 52459f78eb..37b4142073 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -38,7 +38,7 @@ let pp_bracket_comment s = str"{- " ++ hov 0 s ++ str" -}"
 let preamble mod_name comment used_modules usf =
   let pp_import mp = str ("import qualified "^ string_of_modfile mp ^"\n")
   in
-  (if not usf.magic then mt ()
+  (if not (usf.magic || usf.tunknown) then mt ()
    else
      str "{-# OPTIONS_GHC -cpp -XMagicHash #-}" ++ fnl () ++
      str "{- For Hugs, use the option -F\"cpp -P -traditional\" -}")
@@ -52,22 +52,36 @@ let preamble mod_name comment used_modules usf =
   str "import qualified Prelude" ++ fnl () ++
   prlist pp_import used_modules ++ fnl () ++
   (if List.is_empty used_modules then mt () else fnl ()) ++
-  (if not usf.magic then mt ()
+  (if not (usf.magic || usf.tunknown) then mt ()
    else str "\
 \n#ifdef __GLASGOW_HASKELL__\
 \nimport qualified GHC.Base\
 \nimport qualified GHC.Prim\
-\ntype Any = GHC.Prim.Any\
+\n#else\
+\n-- HUGS\
+\nimport qualified IOExts\
+\n#endif" ++ fnl2 ())
+  ++
+  (if not usf.magic then mt ()
+   else str "\
+\n#ifdef __GLASGOW_HASKELL__\
 \nunsafeCoerce :: a -> b\
 \nunsafeCoerce = GHC.Base.unsafeCoerce#\
 \n#else\
 \n-- HUGS\
-\nimport qualified IOExts\
-\ntype Any = ()\
 \nunsafeCoerce :: a -> b\
 \nunsafeCoerce = IOExts.unsafeCoerce\
 \n#endif" ++ fnl2 ())
   ++
+  (if not usf.tunknown then mt ()
+   else str "\
+\n#ifdef __GLASGOW_HASKELL__\
+\ntype Any = GHC.Prim.Any\
+\n#else\
+\n-- HUGS\
+\ntype Any = ()\
+\n#endif" ++ fnl2 ())
+  ++
   (if not usf.mldummy then mt ()
    else str "__ :: any" ++ fnl () ++
         str "__ = Prelude.error \"Logical or arity value used\"" ++ fnl2 ())
@@ -349,7 +363,7 @@ and pp_module_expr = function
   | MEfunctor _ -> mt ()
       (* for the moment we simply discard unapplied functors *)
   | MEident _ | MEapply _ -> assert false
-      (* should be expansed in extract_env *)
+      (* should be expanded in extract_env *)
 
 let pp_struct =
   let pp_sel (mp,sel) =
diff --git a/plugins/extraction/json.ml b/plugins/extraction/json.ml
new file mode 100644
index 0000000000..125dc86b82
--- /dev/null
+++ b/plugins/extraction/json.ml
@@ -0,0 +1,278 @@
+open Pp
+open Errors
+open Util
+open Names
+open Nameops
+open Globnames
+open Table
+open Miniml
+open Mlutil
+open Common
+
+let json_str s =
+  qs s
+
+let json_int i =
+  int i
+
+let json_bool b =
+  if b then str "true" else str "false"
+
+let json_null =
+  str "null"
+
+let json_global typ ref =
+  json_str (Common.pp_global typ ref)
+
+let json_id id =
+  json_str (Id.to_string id)
+
+let json_dict_one (k, v) =
+  json_str k ++ str (": ") ++ v
+
+let json_dict_open l =
+  str ("{") ++ fnl () ++
+  str ("  ") ++ hov 0 (prlist_with_sep pr_comma json_dict_one l)
+
+let json_dict l =
+  json_dict_open l ++ fnl () ++
+  str ("}")
+
+let json_list l =
+  str ("[") ++ fnl () ++
+  str ("  ") ++ hov 0 (prlist_with_sep pr_comma (fun x -> x) l) ++ fnl () ++
+  str ("]")
+
+let json_listarr a =
+  str ("[") ++ fnl () ++
+  str ("  ") ++ hov 0 (prvect_with_sep pr_comma (fun x -> x) a) ++ fnl () ++
+  str ("]")
+
+
+let preamble mod_name comment used_modules usf =
+  (match comment with
+    | None -> mt ()
+    | Some s -> str "/* " ++ hov 0 s ++ str " */" ++ fnl ()) ++
+  json_dict_open [
+    ("what", json_str "module");
+    ("name", json_id mod_name);
+    ("need_magic", json_bool (usf.magic));
+    ("need_dummy", json_bool (usf.mldummy));
+    ("used_modules", json_list
+      (List.map (fun mf -> json_str (file_of_modfile mf)) used_modules))
+  ]
+
+
+(*s Pretty-printing of types. *)
+
+let rec json_type vl = function
+  | Tmeta _ | Tvar' _ -> assert false
+  | Tvar i -> (try
+      let varid = List.nth vl (pred i) in json_dict [
+        ("what", json_str "type:var");
+        ("name", json_id varid)
+      ]
+    with Failure _ -> json_dict [
+        ("what", json_str "type:varidx");
+        ("name", json_int i)
+      ])
+  | Tglob (r, l) -> json_dict [
+      ("what", json_str "type:glob");
+      ("name", json_global Type r);
+      ("args", json_list (List.map (json_type vl) l))
+    ]
+  | Tarr (t1,t2) -> json_dict [
+      ("what", json_str "type:arrow");
+      ("left", json_type vl t1);
+      ("right", json_type vl t2)
+    ]
+  | Tdummy _ -> json_dict [("what", json_str "type:dummy")]
+  | Tunknown -> json_dict [("what", json_str "type:unknown")]
+  | Taxiom -> json_dict [("what", json_str "type:axiom")]
+
+
+(*s Pretty-printing of expressions. *)
+
+let rec json_expr env = function
+  | MLrel n -> json_dict [
+      ("what", json_str "expr:rel");
+      ("name", json_id (get_db_name n env))
+    ]
+  | MLapp (f, args) -> json_dict [
+      ("what", json_str "expr:apply");
+      ("func", json_expr env f);
+      ("args", json_list (List.map (json_expr env) args))
+    ]
+  | MLlam _ as a ->
+    let fl, a' = collect_lams a in
+    let fl, env' = push_vars (List.map id_of_mlid fl) env in
+    json_dict [
+      ("what", json_str "expr:lambda");
+      ("argnames", json_list (List.map json_id (List.rev fl)));
+      ("body", json_expr env' a')
+    ]
+  | MLletin (id, a1, a2) ->
+    let i, env' = push_vars [id_of_mlid id] env in
+    json_dict [
+      ("what", json_str "expr:let");
+      ("name", json_id (List.hd i));
+      ("nameval", json_expr env a1);
+      ("body", json_expr env' a2)
+    ]
+  | MLglob r -> json_dict [
+      ("what", json_str "expr:global");
+      ("name", json_global Term r)
+    ]
+  | MLcons (_, r, a) -> json_dict [
+      ("what", json_str "expr:constructor");
+      ("name", json_global Cons r);
+      ("args", json_list (List.map (json_expr env) a))
+    ]
+  | MLtuple l -> json_dict [
+      ("what", json_str "expr:tuple");
+      ("items", json_list (List.map (json_expr env) l))
+    ]
+  | MLcase (typ, t, pv) -> json_dict [
+      ("what", json_str "expr:case");
+      ("expr", json_expr env t);
+      ("cases", json_listarr (Array.map (fun x -> json_one_pat env x) pv))
+    ]
+  | MLfix (i, ids, defs) ->
+    let ids', env' = push_vars (List.rev (Array.to_list ids)) env in
+    let ids' = Array.of_list (List.rev ids') in
+    json_dict [
+      ("what", json_str "expr:fix");
+      ("funcs", json_listarr (Array.map (fun (fi, ti) ->
+        json_dict [
+          ("what", json_str "fix:item");
+          ("name", json_id fi);
+          ("body", json_function env' ti)
+        ]) (Array.map2 (fun a b -> a,b) ids' defs)))
+    ]
+  | MLexn s -> json_dict [
+      ("what", json_str "expr:exception");
+      ("msg", json_str s)
+    ]
+  | MLdummy -> json_dict [("what", json_str "expr:dummy")]
+  | MLmagic a -> json_dict [
+      ("what", json_str "expr:coerce");
+      ("value", json_expr env a)
+    ]
+  | MLaxiom -> json_dict [("what", json_str "expr:axiom")]
+
+and json_one_pat env (ids,p,t) =
+  let ids', env' = push_vars (List.rev_map id_of_mlid ids) env in json_dict [
+    ("what", json_str "case");
+    ("pat", json_gen_pat (List.rev ids') env' p);
+    ("body", json_expr env' t)
+  ]
+
+and json_gen_pat ids env = function
+  | Pcons (r, l) -> json_cons_pat r (List.map (json_gen_pat ids env) l)
+  | Pusual r -> json_cons_pat r (List.map json_id ids)
+  | Ptuple l -> json_dict [
+      ("what", json_str "pat:tuple");
+      ("items", json_list (List.map (json_gen_pat ids env) l))
+    ]
+  | Pwild -> json_dict [("what", json_str "pat:wild")]
+  | Prel n -> json_dict [
+      ("what", json_str "pat:rel");
+      ("name", json_id (get_db_name n env))
+    ]
+
+and json_cons_pat r ppl = json_dict [
+    ("what", json_str "pat:constructor");
+    ("name", json_global Cons r);
+    ("argnames", json_list ppl)
+  ]
+
+and json_function env t =
+  let bl, t' = collect_lams t in
+  let bl, env' = push_vars (List.map id_of_mlid bl) env in
+  json_dict [
+    ("what", json_str "expr:lambda");
+    ("argnames", json_list (List.map json_id (List.rev bl)));
+    ("body", json_expr env' t')
+  ]
+
+
+(*s Pretty-printing of inductive types declaration. *)
+
+let json_ind ip pl cv = json_dict [
+    ("what", json_str "decl:ind");
+    ("name", json_global Type (IndRef ip));
+    ("argnames", json_list (List.map json_id pl));
+    ("constructors", json_listarr (Array.mapi (fun idx c -> json_dict [
+        ("name", json_global Cons (ConstructRef (ip, idx+1)));
+        ("argtypes", json_list (List.map (json_type pl) c))
+      ]) cv))
+  ]
+
+
+(*s Pretty-printing of a declaration. *)
+
+let pp_decl = function
+  | Dind (kn, defs) -> prvecti_with_sep pr_comma
+    (fun i p -> if p.ip_logical then str ""
+     else json_ind (kn, i) p.ip_vars p.ip_types) defs.ind_packets
+  | Dtype (r, l, t) -> json_dict [
+      ("what", json_str "decl:type");
+      ("name", json_global Type r);
+      ("argnames", json_list (List.map json_id l));
+      ("value", json_type l t)
+    ]
+  | Dfix (rv, defs, typs) -> json_dict [
+      ("what", json_str "decl:fixgroup");
+      ("fixlist", json_listarr (Array.mapi (fun i r ->
+        json_dict [
+          ("what", json_str "fixgroup:item");
+          ("name", json_global Term rv.(i));
+          ("type", json_type [] typs.(i));
+          ("value", json_function (empty_env ()) defs.(i))
+        ]) rv))
+    ]
+  | Dterm (r, a, t) -> json_dict [
+      ("what", json_str "decl:term");
+      ("name", json_global Term r);
+      ("type", json_type [] t);
+      ("value", json_function (empty_env ()) a)
+    ]
+
+let rec pp_structure_elem = function
+  | (l,SEdecl d) -> [ pp_decl d ]
+  | (l,SEmodule m) -> pp_module_expr m.ml_mod_expr
+  | (l,SEmodtype m) -> []
+      (* for the moment we simply discard module type *)
+
+and pp_module_expr = function
+  | MEstruct (mp,sel) -> List.concat (List.map pp_structure_elem sel)
+  | MEfunctor _ -> []
+      (* for the moment we simply discard unapplied functors *)
+  | MEident _ | MEapply _ -> assert false
+      (* should be expansed in extract_env *)
+
+let pp_struct mls =
+  let pp_sel (mp,sel) =
+    push_visible mp [];
+    let p = prlist_with_sep pr_comma identity
+      (List.concat (List.map pp_structure_elem sel)) in
+    pop_visible (); p
+  in
+  str "," ++ fnl () ++
+  str "  " ++ qs "declarations" ++ str ": [" ++ fnl () ++
+  str "    " ++ hov 0 (prlist_with_sep pr_comma pp_sel mls) ++ fnl () ++
+  str "  ]" ++ fnl () ++
+  str "}" ++ fnl ()
+
+
+let json_descr = {
+  keywords = Id.Set.empty;
+  file_suffix = ".json";
+  file_naming = file_of_modfile;
+  preamble = preamble;
+  pp_struct = pp_struct;
+  sig_suffix = None;
+  sig_preamble = (fun _ _ _ _ -> mt ());
+  pp_sig = (fun _ -> mt ());
+  pp_decl = pp_decl;
+}
diff --git a/plugins/extraction/json.mli b/plugins/extraction/json.mli
new file mode 100644
index 0000000000..3ba240a1d0
--- /dev/null
+++ b/plugins/extraction/json.mli
@@ -0,0 +1 @@
+val json_descr : Miniml.language_descr
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index 99b4fd448d..cc8b6d8e79 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -212,7 +212,7 @@ and pp_module_expr = function
   | MEfunctor _ -> mt ()
       (* for the moment we simply discard unapplied functors *)
   | MEident _ | MEapply _ -> assert false
-      (* should be expansed in extract_env *)
+      (* should be expanded in extract_env *)
 
 let pp_struct =
   let pp_sel (mp,sel) =
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 44d760ccdf..a57c39eef1 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -554,7 +554,7 @@ let _ = declare_string_option
 
 (*s Extraction Lang *)
 
-type lang = Ocaml | Haskell | Scheme
+type lang = Ocaml | Haskell | Scheme | JSON
 
 let lang_ref = Summary.ref Ocaml ~name:"ExtrLang"
 
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 1acbe3555f..648f232114 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -142,7 +142,7 @@ val file_comment : unit -> string
 
 (*s Target language. *)
 
-type lang = Ocaml | Haskell | Scheme
+type lang = Ocaml | Haskell | Scheme | JSON
 val lang : unit -> lang
 
 (*s Extraction modes: modular or monolithic, library or minimal ?
diff --git a/plugins/extraction/vo.itarget b/plugins/extraction/vo.itarget
index 1fe09f6fa2..f04890480f 100644
--- a/plugins/extraction/vo.itarget
+++ b/plugins/extraction/vo.itarget
@@ -1,3 +1,4 @@
+ExtrHaskellBasic.vo
 ExtrOcamlBasic.vo
 ExtrOcamlIntConv.vo
 ExtrOcamlBigIntConv.vo
diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v
index 22ddd549e6..8b959c2784 100644
--- a/plugins/micromega/MExtraction.v
+++ b/plugins/micromega/MExtraction.v
@@ -34,7 +34,7 @@ Extract Inductive sumor => option [ Some None ].
    -  rightmost choice (Inright) is (None) *)
 
 
-(** To preserve its laziness, andb is normally expansed.
+(** To preserve its laziness, andb is normally expanded.
     Let's rather use the ocaml && *)
 Extract Inlined Constant andb => "(&&)".
 
diff --git a/plugins/omega/Omega.v b/plugins/omega/Omega.v
index 7400d4629d..a5f90dd66e 100644
--- a/plugins/omega/Omega.v
+++ b/plugins/omega/Omega.v
@@ -13,10 +13,11 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* We do not require [ZArith] anymore, but only what's necessary for Omega *)
+(* We import what is necessary for Omega *)
 Require Export ZArith_base.
 Require Export OmegaLemmas.
 Require Export PreOmega.
+
 Declare ML Module "omega_plugin".
 
 Hint Resolve Z.le_refl Z.add_comm Z.add_assoc Z.mul_comm Z.mul_assoc Z.add_0_l
@@ -25,11 +26,6 @@ Hint Resolve Z.le_refl Z.add_comm Z.add_assoc Z.mul_comm Z.mul_assoc Z.add_0_l
 
 Require Export Zhints.
 
-(*
-(* The constant minus is required in coq_omega.ml *)
-Require Minus.
-*)
-
 Hint Extern 10 (_ = _ :>nat) => abstract omega: zarith.
 Hint Extern 10 (_ <= _) => abstract omega: zarith.
 Hint Extern 10 (_ < _) => abstract omega: zarith.
diff --git a/plugins/omega/OmegaPlugin.v b/plugins/omega/OmegaPlugin.v
index 9e5c148411..9f101dbf2e 100644
--- a/plugins/omega/OmegaPlugin.v
+++ b/plugins/omega/OmegaPlugin.v
@@ -6,4 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(* To strictly import the omega tactic *)
+
+Require ZArith_base.
+Require OmegaLemmas.
+Require PreOmega.
+
 Declare ML Module "omega_plugin".
diff --git a/plugins/omega/OmegaTactic.v b/plugins/omega/OmegaTactic.v
new file mode 100644
index 0000000000..9f101dbf2e
--- /dev/null
+++ b/plugins/omega/OmegaTactic.v
@@ -0,0 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* To strictly import the omega tactic *)
+
+Require ZArith_base.
+Require OmegaLemmas.
+Require PreOmega.
+
+Declare ML Module "omega_plugin".
diff --git a/plugins/omega/vo.itarget b/plugins/omega/vo.itarget
index 9d9a77a8c2..842210e216 100644
--- a/plugins/omega/vo.itarget
+++ b/plugins/omega/vo.itarget
@@ -1,4 +1,5 @@
 OmegaLemmas.vo
 OmegaPlugin.vo
+OmegaTactic.vo
 Omega.vo
 PreOmega.vo