signatures dans le bon ordre

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

2 files changed, 13 insertions, 13 deletions

diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index b3c8a822f8..a8fdbf8ff8 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -120,18 +120,15 @@ let v_of_arity env c = match get_arity env c with
    for example with the types of inductive definitions, which are known
    to be already in arity form. *)
 
-let signature_of_arity = 
-  let rec sign_of acc env c = match kind_of_term c with
-    | IsProd (n, t, c') ->
-	let env' = push_rel (n,None,t) env in
-	let id = id_of_name n in
-	sign_of ((v_of_arity env t, id) :: acc) env' c'
-    | IsSort _ -> 
-	acc
-    | _ ->
-	assert false
-  in
-  sign_of []
+let rec signature_of_arity env c = match kind_of_term c with
+  | IsProd (n, t, c') ->
+      let env' = push_rel (n,None,t) env in
+      let id = id_of_name n in
+      (v_of_arity env t, id) :: (signature_of_arity env' c')
+  | IsSort _ -> 
+      []
+  | _ ->
+      assert false
 
 (* [list_of_ml_arrows] applied to the ML type [a->b->]\dots[z->t]
    returns the list [[a;b;...;z]]. It is used when making the ML types
@@ -242,7 +239,9 @@ let rec extract_type env c =
 		  (match extract_constant sp with
 		     | Emltype (_, sc, flc) -> 
 			 extract_type_app env fl (ConstRef sp,sc,flc) args
-		     | Eprop | Emlterm _ -> 
+		     | Eprop -> 
+			 Tprop
+		     | Emlterm _ -> 
 			 assert false 
 			 (* The head symbol must be of type an arity. *))
 		else 
diff --git a/contrib/extraction/test_extraction.v b/contrib/extraction/test_extraction.v
index 22a2cb99a7..240a8f9ef1 100644
--- a/contrib/extraction/test_extraction.v
+++ b/contrib/extraction/test_extraction.v
@@ -51,3 +51,4 @@ Inductive Finite [U:Type] : (Ensemble U) -> Set :=
    |  Union_is_finite:
       (A: (Ensemble U)) (Finite U A) -> 
       (x: U) ~ (A x) -> (Finite U (Add U A x)).
+Extraction Finite.