From 462c1350ddb2c62de080e17b53fb6f1f00d9e3bf Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Fri, 24 Aug 2012 17:36:38 +0000
Subject: Fix Extraction Implicit on axioms.

There was a small bug causing the type in OCaml commentary not to honor
the implicit declaration, whereas the rest of the code did.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15764 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/extraction/extraction.ml | 17 +++++++++++++++--
 1 file changed, 15 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index fb0e7e7c09..82a6c39336 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -924,6 +924,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 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)
@@ -960,8 +973,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
-- 
cgit v1.2.3