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

2 files changed, 18 insertions, 16 deletions

diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index b234ce1f2..43d14f521 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 = 
diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4
index 731ded8dc..0d7146e68 100644
--- a/contrib/recdef/recdef.ml4
+++ b/contrib/recdef/recdef.ml4
@@ -1164,11 +1164,13 @@ let (com_eqn : identifier ->
     );;
 
 
-let recursive_definition is_mes function_name type_of_f r rec_arg_num eq 
+let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq 
     generate_induction_principle using_lemmas : unit =
   let function_type = interp_constr Evd.empty (Global.env()) type_of_f in
   let env = push_named (function_name,None,function_type) (Global.env()) in
-  let equation_lemma_type = interp_constr Evd.empty env eq in 
+(*   Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *)
+  let equation_lemma_type = interp_gen (OfType None) Evd.empty env ~impls:([],rec_impls) eq in 
+(*   Pp.msgnl (Printer.pr_lconstr equation_lemma_type); *)
   let res_vars,eq' = decompose_prod equation_lemma_type in 
   let res = 
 (*     Pp.msgnl (str "res_var :=" ++ Printer.pr_lconstr_env (push_rel_context (List.map (function (x,t) -> (x,None,t)) res_vars) env) eq'); *)
@@ -1252,10 +1254,10 @@ VERNAC COMMAND EXTEND RecursiveDefinition
 	| None -> 1
 	| Some n -> n 
     in
-    recursive_definition false f type_of_f r rec_arg_num eq (fun _ _ _ _ _  _ _ _ -> ()) []]
+    recursive_definition false f [] type_of_f r rec_arg_num eq (fun _ _ _ _ _  _ _ _ -> ()) []]
 | [ "Recursive" "Definition" ident(f) constr(type_of_f) constr(r) constr(wf)
      "[" ne_constr_list(proof) "]" constr(eq) ] ->
-  [ ignore(proof);ignore(wf);recursive_definition false f type_of_f r 1 eq  (fun  _ _  _ _ _ _ _ _ -> ()) []]
+  [ ignore(proof);ignore(wf);recursive_definition false f [] type_of_f r 1 eq  (fun  _ _  _ _ _ _ _ _ -> ()) []]
 END