diff options
Diffstat (limited to 'contrib/funind/tacinv.ml4')
| -rw-r--r-- | contrib/funind/tacinv.ml4 | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/contrib/funind/tacinv.ml4 b/contrib/funind/tacinv.ml4 index c2410d55..2c7e4d33 100644 --- a/contrib/funind/tacinv.ml4 +++ b/contrib/funind/tacinv.ml4 @@ -378,7 +378,7 @@ let rec proofPrinc mi: constr funind = (* <pcase> Cases b of arrPt end.*) | Case (cinfo, pcase, b, arrPt) -> let prod_pcase,_ = decompose_lam pcase in - let nmeb,_ = List.hd prod_pcase in + let _nmeb,_ = List.hd prod_pcase in let newb'= apply_leqtrpl_t b mi.lst_eqs in let type_of_b = Typing.type_of mi.env mi.sigma b in (* Replace the recursive calls to the function by calls to the constant *) @@ -428,7 +428,7 @@ let rec proofPrinc mi: constr funind = let varnames = List.map snd mi.lst_vars in let nb_vars = List.length varnames in let nb_eqs = List.length mi.lst_eqs in - let eqrels = List.map fst mi.lst_eqs in + let _eqrels = List.map fst mi.lst_eqs in (* [terms_recs]: appel rec du fixpoint, On concatène les appels recs trouvés dans les let in et les Cases avec ceux trouves dans u (ie mi.mimick). *) @@ -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 - + |