Reorganisation of intropattern code

- emphasizing the different kinds of patterns
- factorizing code of the non-naming intro-patterns

Still some questions:

- Should -> and <- apply to hypotheses or not (currently they apply to
  hypotheses either when used in assert-style tactics or apply in, or
  when the term to rewrite is a variable, in which case "subst" is
  applied)?
- Should "subst" be used when the -> or <- rewrites an equation x=t
  posed by "assert" (i.e. rewrite everywhere and clearing x and hyp)?
- Should -> and <- be applicable in non assert-style if the lemma has
  quantifications?

4 files changed, 9 insertions, 6 deletions

diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index f780d1bb50..702d554fc5 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -735,7 +735,7 @@ let consider_tac c hyps gls =
     | _ ->
 	let id = pf_get_new_id (Id.of_string "_tmp") gls in
 	tclTHEN
-	  (Proofview.V82.of_tactic (forward true None (Some (Loc.ghost, IntroIdentifier id)) c))
+	  (Proofview.V82.of_tactic (pose_proof (Name id) c))
  	  (consider_match false [] [id] hyps) gls
 
 
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index d77385321e..5fa689f000 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -83,6 +83,9 @@ let pr_intro_as_pat prc _ _ pat =
       spc () ++ str "as" ++ spc () ++ Miscprint.pr_intro_pattern pat
     | None -> mt ()
 
+let out_disjunctive = function
+  | loc, IntroAction (IntroOrAndPattern l) -> (loc,l)
+  | _ -> Errors.error "Disjunctive or conjunctive intro pattern expected."
 
 ARGUMENT EXTEND with_names TYPED AS simple_intropattern_opt PRINTED BY pr_intro_as_pat
 |   [ "as"  simple_intropattern(ipat) ] -> [ Some ipat ]
@@ -100,7 +103,7 @@ TACTIC EXTEND newfunind
 	 | [c] -> c
 	 | c::cl -> applist(c,cl)
        in
-       Extratactics.onSomeWithHoles (fun x -> Proofview.V82.tactic (functional_induction true c x pat)) princl ]
+       Extratactics.onSomeWithHoles (fun x -> Proofview.V82.tactic (functional_induction true c x (Option.map out_disjunctive pat))) princl ]
 END
 (***** debug only ***)
 TACTIC EXTEND snewfunind
@@ -111,7 +114,7 @@ TACTIC EXTEND snewfunind
 	 | [c] -> c
 	 | c::cl -> applist(c,cl)
        in
-       Extratactics.onSomeWithHoles (fun x -> Proofview.V82.tactic (functional_induction false c x pat)) princl ]
+       Extratactics.onSomeWithHoles (fun x -> Proofview.V82.tactic (functional_induction false c x (Option.map out_disjunctive pat))) princl ]
 END
 
 
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index 91a5ddf826..f88a72ff51 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -10,7 +10,7 @@ val functional_induction :
   bool ->
   Term.constr ->
   (Term.constr * Term.constr bindings) option ->
-  intro_pattern_expr Loc.located option ->
+  or_and_intro_pattern_expr Loc.located option ->
   Proof_type.goal Tacmach.sigma -> Proof_type.goal list Evd.sigma
 
 
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 4fcc65bda9..97157facd0 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -271,7 +271,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
       List.map
 	(fun (_,_,br_type) ->
 	   List.map
-	     (fun id -> Loc.ghost, IntroIdentifier id)
+	     (fun id -> Loc.ghost, IntroNaming (IntroIdentifier id))
 	     (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum br_type))))
 	)
 	branches
@@ -329,7 +329,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
       	List.fold_right
       	  (fun (_,pat) acc ->
       	     match pat with
-	       | IntroIdentifier id -> id::acc
+	       | IntroNaming (IntroIdentifier id) -> id::acc
       	       | _ -> anomaly (Pp.str "Not an identifier")
       	  )
       	  (List.nth intro_pats (pred i))