package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.18.0.tar.gz
md5=8d852367b54f095d9fbabd000304d450
sha512=46922d5f2eb6802a148a52fd3e7f0be8370c93e7bc33cee05cf4a2044290845b10ccddbaa306f29c808e7c5019700763e37e45ff6deb507b874a4348010fed50
doc/src/cc_plugin/g_congruence.ml.html
Source file g_congruence.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62# 11 "plugins/cc/g_congruence.mlg" open Ltac_plugin open Cctac open Stdarg let _ = Mltop.add_known_module "coq-core.plugins.cc" let () = Tacentries.tactic_extend "coq-core.plugins.cc" "cc" ~level:0 [(Tacentries.TyML (Tacentries.TyIdent ("congruence", Tacentries.TyArg ( Extend.TUopt ( Extend.TUentry (Genarg.get_arg_tag wit_natural)), Tacentries.TyNil)), (fun n ist -> # 25 "plugins/cc/g_congruence.mlg" congruence_tac (Option.default 1000 n) [] ))); (Tacentries.TyML (Tacentries.TyIdent ("congruence", Tacentries.TyArg ( Extend.TUopt ( Extend.TUentry (Genarg.get_arg_tag wit_natural)), Tacentries.TyIdent ("with", Tacentries.TyArg ( Extend.TUlist1 ( Extend.TUentry (Genarg.get_arg_tag wit_constr)), Tacentries.TyNil)))), (fun n l ist -> # 27 "plugins/cc/g_congruence.mlg" congruence_tac (Option.default 1000 n) l ))); (Tacentries.TyML (Tacentries.TyIdent ("simple", Tacentries.TyIdent ("congruence", Tacentries.TyArg ( Extend.TUopt ( Extend.TUentry (Genarg.get_arg_tag wit_natural)), Tacentries.TyNil))), (fun n ist -> # 29 "plugins/cc/g_congruence.mlg" simple_congruence_tac (Option.default 1000 n) [] ))); (Tacentries.TyML (Tacentries.TyIdent ("simple", Tacentries.TyIdent ("congruence", Tacentries.TyArg ( Extend.TUopt ( Extend.TUentry (Genarg.get_arg_tag wit_natural)), Tacentries.TyIdent ("with", Tacentries.TyArg ( Extend.TUlist1 ( Extend.TUentry (Genarg.get_arg_tag wit_constr)), Tacentries.TyNil))))), (fun n l ist -> # 31 "plugins/cc/g_congruence.mlg" simple_congruence_tac (Option.default 1000 n) l )))] let () = Tacentries.tactic_extend "coq-core.plugins.cc" "f_equal" ~level:0 [(Tacentries.TyML (Tacentries.TyIdent ("f_equal", Tacentries.TyNil), (fun ist -> # 35 "plugins/cc/g_congruence.mlg" f_equal )))]