diff options
Diffstat (limited to 'contrib/funind/g_indfun.ml4')
| -rw-r--r-- | contrib/funind/g_indfun.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/funind/g_indfun.ml4 b/contrib/funind/g_indfun.ml4 index 654474b32..a79b46d96 100644 --- a/contrib/funind/g_indfun.ml4 +++ b/contrib/funind/g_indfun.ml4 @@ -358,7 +358,7 @@ let poseq_unsafe idunsafe cstr gl = tclTHEN (Tactics.letin_tac None (Name idunsafe) cstr None allClauses) (tclTHENFIRST - (Tactics.assert_as true (Util.dummy_loc,IntroAnonymous) (mkEq typ (mkVar idunsafe) cstr)) + (Tactics.assert_tac Anonymous (mkEq typ (mkVar idunsafe) cstr)) Tactics.reflexivity) gl |