Merge tag 'upstream/8.4pl1dfsg' into experimental/master

Upstream version 8.4pl1dfsg

1 files changed, 26 insertions, 10 deletions

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index e76c6919..0a17453c 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -130,7 +130,7 @@ let rec nb_default_params env c =
 
 (* Enriching a signature with implicit information *)
 
-let sign_with_implicits r s =
+let sign_with_implicits r s nb_params =
   let implicits = implicits_of_global r in
   let rec add_impl i = function
     | [] -> []
@@ -139,7 +139,7 @@ let sign_with_implicits r s =
 	  if sign = Keep && List.mem i implicits then Kill Kother else sign
 	in sign' :: add_impl (succ i) s
   in
-  add_impl 1 s
+  add_impl (1+nb_params) s
 
 (* Enriching a exception message *)
 
@@ -667,20 +667,23 @@ and extract_cst_app env mle mlt kn args =
   let head = put_magic_if magic1 (MLglob (ConstRef kn)) in
   (* Now, the extraction of the arguments. *)
   let s_full = type2signature env (snd schema) in
-  let s_full = sign_with_implicits (ConstRef kn) s_full in
+  let s_full = sign_with_implicits (ConstRef kn) s_full 0 in
   let s = sign_no_final_keeps s_full in
   let ls = List.length s in
   let la = List.length args in
   (* The ml arguments, already expunged from known logical ones *)
   let mla = make_mlargs env mle s args metas in
   let mla =
-    if not magic1 then
+    if magic1 || lang () <> Ocaml then mla
+    else
       try
+        (* for better optimisations later, we discard dependent args
+           of projections and replace them by fake args that will be
+           removed during final pretty-print. *)
 	let l,l' = list_chop (projection_arity (ConstRef kn)) mla in
 	if l' <> [] then (List.map (fun _ -> MLexn "Proj Args") l) @ l'
 	else mla
       with _ -> mla
-    else mla
   in
   (* For strict languages, purely logical signatures with at least
      one [Kill Kother] lead to a dummy lam. So a [MLdummy] is left
@@ -726,7 +729,7 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
   let type_cons = instantiation (nb_tvars, type_cons) in
   (* Then, the usual variables [s], [ls], [la], ... *)
   let s = List.map (type2sign env) types in
-  let s = sign_with_implicits (ConstructRef cp) s in
+  let s = sign_with_implicits (ConstructRef cp) s params_nb in
   let ls = List.length s in
   let la = List.length args in
   assert (la <= ls + params_nb);
@@ -805,7 +808,7 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt =
 	let l = List.map f oi.ip_types.(i) in
 	(* the corresponding signature *)
 	let s = List.map (type2sign env) oi.ip_types.(i) in
-	let s = sign_with_implicits r s in
+	let s = sign_with_implicits r s mi.ind_nparams in
 	(* Extraction of the branch (in functional form). *)
 	let e = extract_maybe_term env mle (type_recomp (l,mlt)) br.(i) in
 	(* We suppress dummy arguments according to signature. *)
@@ -876,7 +879,7 @@ let extract_std_constant env kn body typ =
   let l,t' = type_decomp (expand env (var2var' t)) in
   let s = List.map (type2sign env) l in
   (* Check for user-declared implicit information *)
-  let s = sign_with_implicits (ConstRef kn) s in
+  let s = sign_with_implicits (ConstRef kn) s 0 in
   (* Decomposing the top level lambdas of [body].
      If there isn't enough, it's ok, as long as remaining args
      aren't to be pruned (and initial lambdas aren't to be all
@@ -923,6 +926,19 @@ let extract_std_constant env kn body typ =
   in
   trm, type_expunge_from_sign env s t
 
+(* Extracts the type of an axiom, honors the Extraction Implicit declaration. *)
+let extract_axiom env kn typ =
+  reset_meta_count ();
+  (* The short type [t] (i.e. possibly with abbreviations). *)
+  let t = snd (record_constant_type env kn (Some typ)) in
+  (* The real type [t']: without head products, expanded, *)
+  (* and with [Tvar] translated to [Tvar'] (not instantiable). *)
+  let l,_ = type_decomp (expand env (var2var' t)) in
+  let s = List.map (type2sign env) l in
+  (* Check for user-declared implicit information *)
+  let s = sign_with_implicits (ConstRef kn) s 0 in
+  type_expunge_from_sign env s t
+
 let extract_fixpoint env vkn (fi,ti,ci) =
   let n = Array.length vkn in
   let types = Array.make n (Tdummy Kother)
@@ -959,8 +975,8 @@ let extract_constant env kn cb =
     in Dtype (r, vl, t)
   in
   let mk_ax () =
-    let t = snd (record_constant_type env kn (Some typ)) in
-    Dterm (r, MLaxiom, type_expunge env t)
+    let t = extract_axiom env kn typ in
+    Dterm (r, MLaxiom, t)
   in
   let mk_def c =
     let e,t = extract_std_constant env kn c typ in