diff options
Diffstat (limited to 'contrib/funind/tacinv.ml4')
| -rw-r--r-- | contrib/funind/tacinv.ml4 | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/contrib/funind/tacinv.ml4 b/contrib/funind/tacinv.ml4 index a12f1f01f3..2c7e4d33c3 100644 --- a/contrib/funind/tacinv.ml4 +++ b/contrib/funind/tacinv.ml4 @@ -772,11 +772,6 @@ let invfun_verif c l dorew gl = else error "wrong number of arguments for the function" -TACTIC EXTEND functional_induction - [ "functional" "induction" constr(c) ne_constr_list(l) ] - -> [ invfun_verif c l true ] -END - (* Construction of the functional scheme. *) @@ -847,15 +842,20 @@ let declareFunScheme f fname mutflist = +TACTIC EXTEND functional_induction + [ "old" "functional" "induction" constr(c) ne_constr_list(l) ] + -> [ invfun_verif c l true ] +END + VERNAC COMMAND EXTEND FunctionalScheme - [ "Functional" "Scheme" ident(na) ":=" "Induction" "for" + [ "Old" "Functional" "Scheme" ident(na) ":=" "Induction" "for" ident(c) "with" ne_ident_list(l) ] -> [ declareFunScheme c na l ] -| [ "Functional" "Scheme" ident(na) ":=" "Induction" "for" ident (c) ] +| [ "Old" "Functional" "Scheme" ident(na) ":=" "Induction" "for" ident (c) ] -> [ declareFunScheme c na [] ] END - + |