diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-13 18:02:11 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-18 18:56:38 +0200 |
| commit | 5c82bcd1f87cc893319f2553c81a73c69b13b54d (patch) | |
| tree | 83ca001f700b5fdb48d0fac8e249c08c589a1d15 /plugins/funind/g_indfun.ml4 | |
| parent | d5fece25d8964d5d9fcd55b66164286aeef5fb9f (diff) | |
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?
Diffstat (limited to 'plugins/funind/g_indfun.ml4')
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index d77385321..5fa689f00 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 |