diff options
| author |  Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
| commit | 870075f34dd9fa5792bfbf413afd3b96f17e76a0 (patch) | |
| tree | 0c647056de1832cf1dba5ba58758b9121418e4be /contrib/funind/g_indfun.ml4 | |
| parent | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (diff) | |
Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg
Diffstat (limited to 'contrib/funind/g_indfun.ml4')
| -rw-r--r-- | contrib/funind/g_indfun.ml4 | 14 |
1 files changed, 2 insertions, 12 deletions
diff --git a/contrib/funind/g_indfun.ml4 b/contrib/funind/g_indfun.ml4 index dae76f2d..d435f513 100644 --- a/contrib/funind/g_indfun.ml4 +++ b/contrib/funind/g_indfun.ml4 @@ -90,11 +90,6 @@ END TACTIC EXTEND newfunind ["functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] -> [ - let pat = - match pat with - | None -> IntroAnonymous - | Some pat -> pat - in let c = match cl with | [] -> assert false | [c] -> c @@ -106,11 +101,6 @@ END TACTIC EXTEND snewfunind ["soft" "functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] -> [ - let pat = - match pat with - | None -> IntroAnonymous - | Some pat -> pat - in let c = match cl with | [] -> assert false | [c] -> c @@ -319,7 +309,7 @@ let poseq_unsafe idunsafe cstr gl = tclTHEN (Tactics.letin_tac None (Name idunsafe) cstr allClauses) (tclTHENFIRST - (Tactics.assert_as true IntroAnonymous (mkEq typ (mkVar idunsafe) cstr)) + (Tactics.assert_as true (Util.dummy_loc,IntroAnonymous) (mkEq typ (mkVar idunsafe) cstr)) Tactics.reflexivity) gl @@ -396,7 +386,7 @@ let finduction (oid:identifier option) (heuristic: fapp_info list -> fapp_info l fun gl -> (functional_induction true (applist (info.fname, List.rev !list_constr_largs)) - None IntroAnonymous) gl)) + None None) gl)) nexttac)) ordered_info_list in (* we try each (f t u v) until one does not fail *) (* TODO: try also to mix functional schemes *) |