adaptation de l'extraction aux changements de Christine concernant rec/rect et False_rec

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2448 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 17 insertions, 16 deletions

diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 1f1266287..2ed139b52 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -646,13 +646,18 @@ and extract_case env ctx ip c br =
 	 MLcase (a, Array.mapi extract_branch br)
      | Rprop -> 
 	 (* Logical singleton case: *)
-	 (* [match c with C i j k -> t] becomes [t'] *)
-	 assert (Array.length br = 1);
-	 let (rb,e) = decompose_lam_eta ni.(0) env br.(0) in
-	 let env' = push_rels_assum rb env in 
-	 (* We know that all arguments are logic. *)
-	 let ctx' = iterate (fun l -> false :: l) ni.(0) ctx in 
-	 extract_constr_to_term env' ctx' e)
+	 if Array.length br = 0 then 
+	   MLcase (MLprop, [||]) (* to be recognize later on as an empty case *)
+	 else begin 
+	   (* [match c with C i j k -> t] becomes [t'] *)
+	   assert (Array.length br = 1);
+	   let (rb,e) = decompose_lam_eta ni.(0) env br.(0) in
+	   let env' = push_rels_assum rb env in 
+	   (* We know that all arguments are logic. *)
+	   let ctx' = iterate (fun l -> false :: l) ni.(0) ctx in 
+	   extract_constr_to_term env' ctx' e
+	 end)
+
   
 (* Extraction of a (co)-fixpoint *)
 
@@ -904,11 +909,7 @@ and extract_inductive_declaration sp =
 
 (*s Extraction of a global reference i.e. a constant or an inductive. *)
 
-let false_rec_sp = path_of_string "Coq.Init.Specif.False_rec"
-let false_rec_e = MLlam (prop_name, MLexn "[False_rec]")
-
 let extract_declaration r = match r with
-  | ConstRef sp when sp = false_rec_sp -> Dglob (r, false_rec_e)
   | ConstRef sp -> 
       (match extract_constant sp with
 	 | Emltype (mlt, s, vl) -> Dabbrev (r, List.rev vl, mlt)
diff --git a/contrib/extraction/test/custom/Adalloc b/contrib/extraction/test/custom/Adalloc
index f94ba220b..11cabe4f4 100644
--- a/contrib/extraction/test/custom/Adalloc
+++ b/contrib/extraction/test/custom/Adalloc
@@ -1,4 +1,4 @@
 Require Addr.
 Extraction NoInline ad_double ad_double_plus_un.
 Require Map.
-Extraction Inline Map_rec.
+Extraction Inline Map_rec Map_rect.
diff --git a/contrib/extraction/test/custom/Fset b/contrib/extraction/test/custom/Fset
index c0be70a80..cb2aa8868 100644
--- a/contrib/extraction/test/custom/Fset
+++ b/contrib/extraction/test/custom/Fset
@@ -1,2 +1,2 @@
 Require Map.
-Extraction Inline Map_rec.
+Extraction Inline Map_rec Map_rect.
diff --git a/contrib/extraction/test/custom/Mapcard b/contrib/extraction/test/custom/Mapcard
index af5c23daa..71496aba9 100644
--- a/contrib/extraction/test/custom/Mapcard
+++ b/contrib/extraction/test/custom/Mapcard
@@ -3,4 +3,4 @@ Extraction NoInline plus_is_one.
 Require Addr.
 Extraction NoInline ad_double ad_double_plus_un.
 Require Map.
-Extraction Inline Map_rec.
+Extraction Inline Map_rec Map_rect.
diff --git a/contrib/extraction/test/custom/Mapiter b/contrib/extraction/test/custom/Mapiter
index ad4a58735..ef57348fb 100644
--- a/contrib/extraction/test/custom/Mapiter
+++ b/contrib/extraction/test/custom/Mapiter
@@ -1,4 +1,4 @@
 Require Addr. 
 Extraction NoInline ad_double ad_double_plus_un.
 Require Map.
-Extraction Inline Map_rec.
+Extraction Inline Map_rec Map_rect.
diff --git a/contrib/extraction/test/custom/all b/contrib/extraction/test/custom/all
index 4e32680ff..14bb482ca 100644
--- a/contrib/extraction/test/custom/all
+++ b/contrib/extraction/test/custom/all
@@ -1 +1 @@
-Extraction Inline sigS_rec prod_rec.
+Extraction Inline sigS_rec sigS_rect prod_rec prod_rect.