Gestion des arguments implicites dans les Functions bien fondees

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

1 files changed, 12 insertions, 12 deletions

diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index b234ce1f23..43d14f5211 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -186,7 +186,7 @@ let build_newrecursive
 	States.unfreeze fs; raise e in
     States.unfreeze fs; def
   in
-  recdef
+  recdef,rec_impls
 	
 
 let compute_annot (name,annot,args,types,body) =
@@ -330,7 +330,7 @@ let generate_principle
 	    Pp.msg_warning 
 	    (str "Cannot define graph(s) for " ++ 
 	       h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
-	       if do_observe () then Cerrors.explain_exn e else mt ())
+	       if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt ())
       | Defining_principle e -> 
 	    Pp.msg_warning
 	    (str "Cannot define principle(s) for "++ 
@@ -360,7 +360,7 @@ let generate_correction_proof_wf f_ref tcc_lemma_ref
     tcc_lemma_ref is_mes  rec_arg_num rec_arg_type relation
 
 
-let register_wf ?(is_mes=false) fname wf_rel_expr wf_arg using_lemmas args ret_type body
+let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas args ret_type body
     pre_hook 
     =  
   let type_of_f = Command.generalize_constr_expr ret_type args in 
@@ -379,13 +379,13 @@ let register_wf ?(is_mes=false) fname wf_rel_expr wf_arg using_lemmas args ret_t
   in
   let unbounded_eq = 
     let f_app_args = 
-      Topconstr.CApp 
+      Topconstr.CAppExpl 
 	(dummy_loc, 
-	 (None,Topconstr.mkIdentC fname) ,
+	 (None,(Ident (dummy_loc,fname))) ,
 	 (List.map 
 	    (function
 	       | _,Anonymous -> assert false 
-	       | _,Name e -> (Topconstr.mkIdentC e,None)
+	       | _,Name e -> (Topconstr.mkIdentC e)
 	    ) 
 	    (Topconstr.names_of_local_assums args)
 	 )
@@ -408,7 +408,7 @@ let register_wf ?(is_mes=false) fname wf_rel_expr wf_arg using_lemmas args ret_t
       ()
   in 
   Recdef.recursive_definition 
-    is_mes fname 
+    is_mes fname rec_impls
     type_of_f
     wf_rel_expr
     rec_arg_num
@@ -417,7 +417,7 @@ let register_wf ?(is_mes=false) fname wf_rel_expr wf_arg using_lemmas args ret_t
     using_lemmas
 
     
-let register_mes fname wf_mes_expr wf_arg using_lemmas args ret_type body = 
+let register_mes fname rec_impls wf_mes_expr wf_arg using_lemmas args ret_type body = 
   let wf_arg_type,wf_arg = 
     match wf_arg with 
       | None -> 
@@ -456,12 +456,12 @@ let register_mes fname wf_mes_expr wf_arg using_lemmas args ret_type body =
   let wf_rel_from_mes = 
     Topconstr.mkAppC(Topconstr.mkRefC  ltof,[wf_arg_type;fun_from_mes])
   in
-  register_wf ~is_mes:true fname wf_rel_from_mes (Some wf_arg) 
+  register_wf ~is_mes:true fname rec_impls wf_rel_from_mes (Some wf_arg) 
     using_lemmas args ret_type body
 	  
 
 let do_generate_principle register_built interactive_proof fixpoint_exprl  = 
-  let recdefs = build_newrecursive fixpoint_exprl in 
+  let recdefs,rec_impls = build_newrecursive fixpoint_exprl in 
   let _is_struct = 
     match fixpoint_exprl with 
       | [((name,Some (Wf (wf_rel,wf_x,using_lemmas)),args,types,body))] -> 
@@ -475,7 +475,7 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl  =
 	      false
 	  in 
 	  if register_built 
-	  then register_wf name wf_rel wf_x using_lemmas args types body pre_hook;
+	  then register_wf name rec_impls wf_rel wf_x using_lemmas args types body pre_hook;
 	  false
       | [((name,Some (Mes (wf_mes,wf_x,using_lemmas)),args,types,body))] -> 
 	  let pre_hook = 
@@ -488,7 +488,7 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl  =
 	      false
 	  in 
 	  if register_built 
-	  then register_mes name wf_mes wf_x using_lemmas args types body pre_hook;
+	  then register_mes name rec_impls wf_mes wf_x using_lemmas args types body pre_hook;
 	  false
       | _ -> 
 	  let fix_names =