gros changement dans mlutil.ml: ajout d'une elimination globale des prop

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

1 files changed, 7 insertions, 3 deletions

diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 2ed139b52..7b2e4c9d7 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -205,7 +205,9 @@ let sign_of_arity env c =
 let vl_of_lbinders = 
   lbinders_fold 
     (fun n _ v a -> 
-       if v = info_arity then (next_ident_away (id_of_name n) (prop_name::a))::a else a) []
+       if v = info_arity 
+       then (next_ident_away (id_of_name n) (prop_name::a))::a 
+       else a) []
   
 let vl_of_arity env c = vl_of_lbinders env (List.rev (fst (decompose_prod c)))
 	 
@@ -542,7 +544,8 @@ and extract_term_info_wt env ctx c t =
    match kind_of_term c with
      | Lambda (n, t, d) ->
 	 let v = v_of_t env t in 
-	 let id = next_ident_away (id_of_name n) [prop_name] in 
+	 let id = id_of_name n in 
+	 let id = if id=prop_name then anonymous else id in 
 	 let env' = push_rel_assum (Name id,t) env in
 	 let ctx' = (snd v = NotArity) :: ctx in
 	 let d' = extract_term_info env' ctx' d in
@@ -553,7 +556,8 @@ and extract_term_info_wt env ctx c t =
             | Info,NotArity -> MLlam (id, d'))
      | LetIn (n, c1, t1, c2) ->
 	 let v = v_of_t env t1 in
-	 let id = next_ident_away (id_of_name n) [prop_name] in 
+	 let id = id_of_name n in 
+	 let id = if id=prop_name then anonymous else id in 
 	 let env' = push_rel (Name id,Some c1,t1) env in
 	 (match v with
 	    | (Info, NotArity) ->