7 files changed, 17 insertions, 17 deletions
diff --git a/plugins/extraction/CHANGES b/plugins/extraction/CHANGES
index 4bc3dba36e..bc7e1448f7 100644
--- a/plugins/extraction/CHANGES
+++ b/plugins/extraction/CHANGES
@@ -200,7 +200,7 @@ For the moment there are:
 	Wf.well_founded_induction
 	Wf.well_founded_induction_type
 Those constants does not match the auto-inlining criterion based on strictness.
-Of course, you can still overide this behaviour via some Extraction NoInline. 
+Of course, you can still override this behaviour via some Extraction NoInline. 
 
 * There is now a web page showing the extraction of all standard theories: 
 http://www.lri.fr/~letouzey/extraction
diff --git a/plugins/extraction/ExtrOcamlBasic.v b/plugins/extraction/ExtrOcamlBasic.v
index 36bb1148b6..02da168fd0 100644
--- a/plugins/extraction/ExtrOcamlBasic.v
+++ b/plugins/extraction/ExtrOcamlBasic.v
@@ -26,9 +26,9 @@ Extract Inductive prod => "( * )" [ "" ].
 Extract Inductive sumbool => bool [ true false ].
 Extract Inductive sumor => option [ Some None ].
 
-(** Restore lazyness of andb, orb.
+(** Restore laziness of andb, orb.
     NB: without these Extract Constant, andb/orb would be inlined
-    by extraction in order to have lazyness, producing inelegant
+    by extraction in order to have laziness, producing inelegant
     (if ... then ... else false) and (if ... then true else ...).
 *)
 
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 59c57cc544..f46d09e335 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -573,7 +573,7 @@ let pp_ocaml_gen k mp rls olab =
 	if is_mp_bound base then pp_ocaml_bound base rls
 	else pp_ocaml_extern k base rls
 
-(* For Haskell, things are simplier: we have removed (almost) all structures *)
+(* For Haskell, things are simpler: we have removed (almost) all structures *)
 
 let pp_haskell_gen k mp rls = match rls with
   | [] -> assert false
@@ -590,7 +590,7 @@ let pp_global k r =
   let s = List.hd ls in
   let mp,l = repr_of_r r in
   if ModPath.equal mp (top_visible_mp ()) then
-    (* simpliest situation: definition of r (or use in the same context) *)
+    (* simplest situation: definition of r (or use in the same context) *)
     (* we update the visible environment *)
     (add_visible (k,s) l; unquote s)
   else
@@ -607,7 +607,7 @@ let pp_module mp =
   let ls = mp_renaming mp in
   match mp with
     | MPdot (mp0,l) when ModPath.equal mp0 (top_visible_mp ()) ->
-	(* simpliest situation: definition of mp (or use in the same context) *)
+        (* simplest situation: definition of mp (or use in the same context) *)
 	(* we update the visible environment *)
 	let s = List.hd ls in
 	add_visible (Mod,s) l; s
diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli
index d27c79cb62..bf98f8cd70 100644
--- a/plugins/extraction/extraction.mli
+++ b/plugins/extraction/extraction.mli
@@ -16,9 +16,9 @@ open Environ
 open Evd
 open Miniml
 
-val extract_constant : env -> Constant.t -> constant_body -> ml_decl
+val extract_constant : env -> Constant.t -> Opaqueproof.opaque constant_body -> ml_decl
 
-val extract_constant_spec : env -> Constant.t -> constant_body -> ml_spec
+val extract_constant_spec : env -> Constant.t -> 'a constant_body -> ml_spec
 
 (** For extracting "module ... with ..." declaration *)
 
diff --git a/plugins/extraction/g_extraction.mlg b/plugins/extraction/g_extraction.mlg
index d7bb27f121..db1a389fe7 100644
--- a/plugins/extraction/g_extraction.mlg
+++ b/plugins/extraction/g_extraction.mlg
@@ -93,7 +93,7 @@ VERNAC COMMAND EXTEND Extraction CLASSIFIED AS QUERY
 END
 
 VERNAC COMMAND EXTEND SeparateExtraction CLASSIFIED AS QUERY
-(* Same, with content splitted in several files *)
+(* Same, with content split in several files *)
 | [ "Separate" "Extraction" ne_global_list(l) ]
   -> { separate_extraction l }
 END
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 399a77c596..c2c48f9565 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -101,7 +101,7 @@ let labels_of_ref r =
 
 (*S The main tables: constants, inductives, records, ... *)
 
-(* Theses tables are not registered within coq save/undo mechanism
+(* These tables are not registered within coq save/undo mechanism
    since we reset their contents at each run of Extraction *)
 
 (* We use [constant_body] (resp. [mutual_inductive_body]) as checksum
@@ -109,7 +109,7 @@ let labels_of_ref r =
 
 (*s Constants tables. *)
 
-let typedefs = ref (Cmap_env.empty : (constant_body * ml_type) Cmap_env.t)
+let typedefs = ref (Cmap_env.empty : (Opaqueproof.opaque constant_body * ml_type) Cmap_env.t)
 let init_typedefs () = typedefs := Cmap_env.empty
 let add_typedef kn cb t =
   typedefs := Cmap_env.add kn (cb,t) !typedefs
@@ -120,7 +120,7 @@ let lookup_typedef kn cb =
   with Not_found -> None
 
 let cst_types =
-  ref (Cmap_env.empty : (constant_body * ml_schema) Cmap_env.t)
+  ref (Cmap_env.empty : (Opaqueproof.opaque constant_body * ml_schema) Cmap_env.t)
 let init_cst_types () = cst_types := Cmap_env.empty
 let add_cst_type kn cb s = cst_types := Cmap_env.add kn (cb,s) !cst_types
 let lookup_cst_type kn cb =
@@ -842,7 +842,7 @@ let in_customs : GlobRef.t * string list * string -> obj =
     ~subst:(Some (fun (s,(r,ids,str)) -> (fst (subst_global s r), ids, str)))
 
 let in_custom_matchs : GlobRef.t * string -> obj =
-  declare_object @@ superglobal_object_nodischarge "ML extractions custom matchs"
+  declare_object @@ superglobal_object_nodischarge "ML extractions custom matches"
     ~cache:(fun (_,(r,s)) -> add_custom_match r s)
     ~subst:(Some (fun (subs,(r,s)) -> (fst (subst_global subs r), s)))
 
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index acc1bfee8a..7e53964642 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -72,11 +72,11 @@ val labels_of_ref : GlobRef.t -> ModPath.t * Label.t list
    [mutual_inductive_body] as checksum. In both case, we should ideally
    also check the env *)
 
-val add_typedef : Constant.t -> constant_body -> ml_type -> unit
-val lookup_typedef : Constant.t -> constant_body -> ml_type option
+val add_typedef : Constant.t -> Opaqueproof.opaque constant_body -> ml_type -> unit
+val lookup_typedef : Constant.t -> Opaqueproof.opaque constant_body -> ml_type option
 
-val add_cst_type : Constant.t -> constant_body -> ml_schema -> unit
-val lookup_cst_type : Constant.t -> constant_body -> ml_schema option
+val add_cst_type : Constant.t -> Opaqueproof.opaque constant_body -> ml_schema -> unit
+val lookup_cst_type : Constant.t -> Opaqueproof.opaque constant_body -> ml_schema option
 
 val add_ind : MutInd.t -> mutual_inductive_body -> ml_ind -> unit
 val lookup_ind : MutInd.t -> mutual_inductive_body -> ml_ind option