+ timide essai pour le traitement des as dans les patterns lors de la generation des graphes de Function

+ Correction d'un petit bug dans les lemmes d'inversions de Function
+ Nettoyage d'hypotheses inutile dans les obligations de preuve de Function (wf et measure). 



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

1 files changed, 23 insertions, 0 deletions

diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4
index 93db0eab21..16067e6f36 100644
--- a/contrib/recdef/recdef.ml4
+++ b/contrib/recdef/recdef.ml4
@@ -745,8 +745,31 @@ let build_and_l l =
 	  ],nb+1
   in f l
 
+
+let is_rec_res id = 
+  let rec_res_name = string_of_id rec_res_id   in 
+  let id_name = string_of_id id in 
+  try 
+    String.sub id_name 0 (String.length rec_res_name) = rec_res_name 
+  with _ -> false
+
+let clear_goals = 
+  let rec clear_goal t = 
+    match kind_of_term t with 
+      | Prod(Name id as na,t,b) -> 
+	  let b' = clear_goal b in 
+	  if noccurn 1 b' && (is_rec_res id) 
+	  then pop b' 
+	  else if b' == b then t 
+	  else mkProd(na,t,b')
+      | _ -> map_constr clear_goal t
+  in 
+  List.map clear_goal 
+
+
 let build_new_goal_type () = 
   let sub_gls_types = get_current_subgoals_types () in 
+  let sub_gls_types = clear_goals sub_gls_types in 
   let res = build_and_l sub_gls_types in 
   res