small changes

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

2 files changed, 27 insertions, 19 deletions

diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4
index c4f0c0ad6f..2bad9bb504 100644
--- a/contrib/funind/indfun_main.ml4
+++ b/contrib/funind/indfun_main.ml4
@@ -13,13 +13,7 @@ open Topconstr
 open Indfun_common 
 open Indfun
 open Genarg
-
-TACTIC EXTEND newfuninv
-   [ "functional" "inversion" ident(hyp) ident(fname) ] -> 
-     [
-       Invfun.invfun hyp fname
-     ]
-END
+open Pcoq
 
 
 let pr_fun_ind_using  prc _ _ opt_c = 
@@ -27,6 +21,7 @@ let pr_fun_ind_using  prc _ _ opt_c =
     | None -> mt ()
     | Some c -> spc () ++ hov 2 (str "using" ++ spc () ++ prc c)
 
+
 ARGUMENT EXTEND fun_ind_using
   TYPED AS constr_opt
   PRINTED BY pr_fun_ind_using
@@ -34,11 +29,33 @@ ARGUMENT EXTEND fun_ind_using
 | [ ] -> [ None ]
 END
 
-let pr_intro_as_pat prc _ _ pat = 
-  str "as" ++ spc () ++ pr_intro_pattern pat
 
+TACTIC EXTEND newfuninv
+   [ "functional" "inversion" ident(hyp) ident(fname) fun_ind_using(princl)] -> 
+     [
+       fun g -> 
+	 let fconst = const_of_id fname in
+	 let princ = 
+	   match princl with 
+	     | None -> 
+		 let f_ind_id =  
+		   (
+		     Indrec.make_elimination_ident
+		       fname 
+		       (Tacticals.elimination_sort_of_goal g)
+		   )
+	       in
+		 let princ = const_of_id f_ind_id in
+		 princ
+	     | Some princ -> destConst princ
+	 in       
+	 Invfun.invfun hyp fconst princ g
+     ]
+END
 
 
+let pr_intro_as_pat prc _ _ pat = 
+  str "as" ++ spc () ++ pr_intro_pattern pat
 
 
 ARGUMENT EXTEND with_names TYPED AS intro_pattern PRINTED BY pr_intro_as_pat
diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml
index 1f711297aa..85a60bd1c0 100644
--- a/contrib/funind/invfun.ml
+++ b/contrib/funind/invfun.ml
@@ -88,18 +88,9 @@ let gen_fargs fargs : tactic =
       g 
       
 
-let invfun (hypname:identifier) (fid:identifier) : tactic=
+let invfun (hypname:identifier) fname princ : tactic=
   fun g -> 
     let nprod_goal = nb_prod (pf_concl g) in
-    let f_ind_id =  
-      (
-	Indrec.make_elimination_ident
-	  fid 
-	  (Tacticals.elimination_sort_of_goal g)
-      )
-    in
-    let fname = const_of_id fid in
-    let princ = const_of_id f_ind_id in
     let princ_info = 
       let princ_type = 
 	(try (match (Global.lookup_constant princ) with