diff options
Diffstat (limited to 'contrib/funind/tacinv.ml4')
| -rw-r--r-- | contrib/funind/tacinv.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/funind/tacinv.ml4 b/contrib/funind/tacinv.ml4 index 517e92d93..27c0658d2 100644 --- a/contrib/funind/tacinv.ml4 +++ b/contrib/funind/tacinv.ml4 @@ -772,8 +772,8 @@ let invfun_verif c l dorew gl = else error "wrong number of arguments for the function" -TACTIC EXTEND FunctionalInduction - [ "Functional" "Induction" constr(c) ne_constr_list(l) ] +TACTIC EXTEND functional_induction + [ "functional" "induction" constr(c) ne_constr_list(l) ] -> [ invfun_verif c l true ] END |