inductifs vides

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

3 files changed, 15 insertions, 29 deletions

diff --git a/contrib/extraction/BUGS b/contrib/extraction/BUGS
index 3c3345da7f..8b13789179 100644
--- a/contrib/extraction/BUGS
+++ b/contrib/extraction/BUGS
@@ -1,22 +1 @@
 
-======================================================================
-
-Coq < Extraction Module Specif.
-Anomaly: Failure "nth". Please report.
-
-======================================================================
-
-Coq < Extraction Module Datatypes.
-
-donne le code suivant :
-
-type coq_Empty_set =
-
-let coq_Empty_set_ind =
-  prop
-
-let coq_Empty_set_rec = function
-
-let coq_Empty_set_rect = function
-  
-======================================================================
diff --git a/contrib/extraction/TODO b/contrib/extraction/TODO
index 376f522516..3bef008046 100644
--- a/contrib/extraction/TODO
+++ b/contrib/extraction/TODO
@@ -1,5 +1,5 @@
 
- 1. Inductifs vides
-
  2. Inductifs singletons
 
+ 3. Axiomes
+
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index cdbf108500..560c757a6d 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -227,7 +227,10 @@ and pp_pat env pv =
 	     end;
 	     'sTR " ->"; 'sPC; pp_expr par env' [] t >]
   in 
-  [< prvect_with_sep (fun () -> [< 'fNL; 'sTR "| " >]) pp_one_pat pv >]
+  if pv = [||] then
+    [< 'sTR "_ -> assert false (* empty inductive *)" >]
+  else
+    [< prvect_with_sep (fun () -> [< 'fNL; 'sTR "| " >]) pp_one_pat pv >]
 
 (*s names of the functions ([ids]) are already pushed in [env],
     and passed here just for convenience. *)
@@ -292,13 +295,17 @@ let pp_one_inductive (pl,name,cl) =
       	       	    prlist_with_sep 
 		      (fun () -> [< 'sPC ; 'sTR "* " >]) pp_type l >] >] 
   in
-  [< pp_parameters pl; P.pp_global name; 'sTR " ="; 'fNL;
-     v 0 [< 'sTR "    ";
-	    prlist_with_sep (fun () -> [< 'fNL; 'sTR "  | " >])
-                            (fun c -> hOV 2 (pp_constructor c)) cl >] >]
+    [< pp_parameters pl; P.pp_global name; 'sTR " ="; 
+       if cl = [] then
+	 [< 'sTR " unit (* empty inductive *)" >]
+       else
+	 [< 'fNL;
+	    v 0 [< 'sTR "    ";
+		   prlist_with_sep (fun () -> [< 'fNL; 'sTR "  | " >])
+                     (fun c -> hOV 2 (pp_constructor c)) cl >] >] >]
 
 let pp_inductive il =
-  [< 'sTR "type " ;
+  [< 'sTR "type ";
      prlist_with_sep 
        (fun () -> [< 'fNL; 'sTR "and " >])
        (fun i -> pp_one_inductive i)