correction of bug #1220

adding a "using" optional argument to Function.


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

2 files changed, 35 insertions, 13 deletions

diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 9a8d52eb7..b234ce1f2 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -129,8 +129,8 @@ let functional_induction with_clean c princl pat =
 
 type annot = 
     Struct of identifier 
-  | Wf of Topconstr.constr_expr * identifier option
-  | Mes of Topconstr.constr_expr * identifier option
+  | Wf of Topconstr.constr_expr * identifier option * Topconstr.constr_expr list
+  | Mes of Topconstr.constr_expr * identifier option * Topconstr.constr_expr list
 
 
 type newfixpoint_expr =
@@ -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 args ret_type body
+let register_wf ?(is_mes=false) fname 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 
@@ -414,9 +414,10 @@ let register_wf ?(is_mes=false) fname wf_rel_expr wf_arg args ret_type body
     rec_arg_num
     eq
     hook
+    using_lemmas
 
     
-let register_mes fname wf_mes_expr wf_arg args ret_type body = 
+let register_mes fname wf_mes_expr wf_arg using_lemmas args ret_type body = 
   let wf_arg_type,wf_arg = 
     match wf_arg with 
       | None -> 
@@ -455,14 +456,15 @@ let register_mes fname wf_mes_expr wf_arg 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) args ret_type body
+  register_wf ~is_mes:true fname 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 _is_struct = 
     match fixpoint_exprl with 
-      | [((name,Some (Wf (wf_rel,wf_x)),args,types,body))] -> 
+      | [((name,Some (Wf (wf_rel,wf_x,using_lemmas)),args,types,body))] -> 
 	  let pre_hook = 
 	    generate_principle 
 	      true
@@ -472,9 +474,10 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl  =
 	      true
 	      false
 	  in 
-	  if register_built then register_wf name wf_rel wf_x args types body pre_hook;
+	  if register_built 
+	  then register_wf name wf_rel wf_x using_lemmas args types body pre_hook;
 	  false
-      | [((name,Some (Mes (wf_mes,wf_x)),args,types,body))] -> 
+      | [((name,Some (Mes (wf_mes,wf_x,using_lemmas)),args,types,body))] -> 
 	  let pre_hook = 
 	    generate_principle 
 	      true
@@ -484,7 +487,8 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl  =
 	      true
 	      false
 	  in 
-	  if register_built then register_mes name wf_mes wf_x args types body pre_hook;
+	  if register_built 
+	  then register_mes name wf_mes wf_x using_lemmas args types body pre_hook;
 	  false
       | _ -> 
 	  let fix_names = 
diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4
index d0be12288..6476340a6 100644
--- a/contrib/funind/indfun_main.ml4
+++ b/contrib/funind/indfun_main.ml4
@@ -103,10 +103,28 @@ TACTIC EXTEND snewfunind
 END
 
 
+let pr_constr_coma_sequence prc _ _ = Util.prlist_with_sep Util.pr_coma prc
+
+ARGUMENT EXTEND constr_coma_sequence'
+  TYPED AS constr_list
+  PRINTED BY pr_constr_coma_sequence
+| [ constr(c) "," constr_coma_sequence'(l) ] -> [ c::l ]
+| [ constr(c) ] -> [ [c] ]
+END
+
+let pr_auto_using prc _prlc _prt = Pptactic.pr_auto_using prc
+
+ARGUMENT EXTEND auto_using'
+  TYPED AS constr_list
+  PRINTED BY pr_auto_using
+| [ "using" constr_coma_sequence'(l) ] -> [ l ]
+| [ ] -> [ [] ]
+END
+
 VERNAC ARGUMENT EXTEND rec_annotation2
   [ "{"  "struct" ident(id)  "}"] -> [ Struct id ]
-| [ "{" "wf" constr(r) ident_opt(id) "}" ] -> [ Wf(r,id) ]
-| [ "{" "measure" constr(r) ident_opt(id) "}" ] -> [ Mes(r,id) ] 
+| [ "{" "wf" constr(r) ident_opt(id) auto_using'(l) "}" ] -> [ Wf(r,id,l) ]
+| [ "{" "measure" constr(r) ident_opt(id) auto_using'(l) "}" ] -> [ Mes(r,id,l) ] 
 END
 
 
@@ -131,8 +149,8 @@ VERNAC ARGUMENT EXTEND rec_definition2
      let check_exists_args an =
        try 
 	 let id = match an with 
-	   | Struct id -> id | Wf(_,Some id) -> id | Mes(_,Some id) -> id 
-	   | Wf(_,None) | Mes(_,None) -> failwith "check_exists_args" 
+	   | Struct id -> id | Wf(_,Some id,_) -> id | Mes(_,Some id,_) -> id 
+	   | Wf(_,None,_) | Mes(_,None,_) -> failwith "check_exists_args" 
 	 in 
 	 (try ignore(Util.list_index (Name id) names - 1); annot
 	  with Not_found ->  Util.user_err_loc