underscores pour les variables représentant des propositions

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

4 files changed, 10 insertions, 3 deletions

diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 661cfef3d..85a448057 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -432,7 +432,6 @@ and extract_term_with_type env ctx c t =
     Rprop
   else match kind_of_term c with
     | IsLambda (n, t, d) ->
-	let id = id_of_name n in
 	let v = v_of_arity env t in 
 	let env' = push_rel (n,None,t) env in
 	let ctx' = (snd v = NotArity) :: ctx in
@@ -440,8 +439,10 @@ and extract_term_with_type env ctx c t =
 	(* If [d] was of type an arity, [c] too would be so *)
 	(match v with
 	   | _,Arity -> d'
-	   | _,NotArity -> match d' with
-	       | Rmlterm a -> Rmlterm (MLlam (id, a))
+	   | l,NotArity -> match d' with
+	       | Rmlterm a -> 
+		   let id = if l = Logic then prop_name else id_of_name n in
+		   Rmlterm (MLlam (id, a))
 	       | Rprop -> assert false (* Cf. rem. above *))
     | IsRel n ->
 	(* TODO : magic or not *) 
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index f1876bdc3..7f5b23901 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -148,6 +148,7 @@ let rec decomp_app = function
       assert false
 
 let anonymous = Names.id_of_string "x"
+let prop_name = Names.id_of_string "_"
 
 let rec n_lam n a =
   if n = 0 then a else MLlam (anonymous, n_lam (pred n) a)
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
index 3bbe8f8a3..b60a3fdf9 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -2,6 +2,7 @@
 open Miniml
 
 val anonymous : Names.identifier
+val prop_name : Names.identifier
 
 val occurs : int -> ml_ast -> bool
 
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 560c757a6..bded16d1d 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -84,6 +84,10 @@ type env = identifier list * Idset.t
 let rec rename_vars avoid = function
   | [] -> 
       [], avoid
+  | id :: idl when id == prop_name ->
+      (* we don't rename propositions binders *)
+      let (idl', avoid') = rename_vars avoid idl in
+      (id :: idl', avoid')
   | id :: idl ->
       let id' = rename_id (lowercase_id id) avoid in
       let (idl', avoid') = rename_vars (Idset.add id' avoid) idl in