package coq
Formal proof management system
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.14.1.tar.gz
sha256=3cbfc1e1a72b16d4744f5b64ede59586071e31d9c11c811a0372060727bfd9c3
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 63 64 65 66 67 68# 11 "plugins/cc/g_congruence.mlg" open Ltac_plugin open Cctac open Stdarg let __coq_plugin_name = "cc_plugin" let _ = Mltop.add_known_module __coq_plugin_name let () = Tacentries.tactic_extend __coq_plugin_name "cc" ~level:0 [(Tacentries.TyML ( Tacentries.TyIdent ("congruence", Tacentries.TyNil), (fun ist -> # 24 "plugins/cc/g_congruence.mlg" congruence_tac 1000 [] ))); (Tacentries.TyML ( Tacentries.TyIdent ("congruence", Tacentries.TyArg ( Extend.TUentry (Genarg.get_arg_tag wit_natural), Tacentries.TyNil)), (fun n ist -> # 25 "plugins/cc/g_congruence.mlg" congruence_tac n [] ))); (Tacentries.TyML ( Tacentries.TyIdent ("congruence", Tacentries.TyIdent ("with", Tacentries.TyArg ( Extend.TUlist1 ( Extend.TUentry (Genarg.get_arg_tag wit_constr)), Tacentries.TyNil))), (fun l ist -> # 26 "plugins/cc/g_congruence.mlg" congruence_tac 1000 l ))); (Tacentries.TyML ( Tacentries.TyIdent ("congruence", Tacentries.TyArg ( 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 -> # 28 "plugins/cc/g_congruence.mlg" congruence_tac n l )))] let () = Tacentries.tactic_extend __coq_plugin_name "f_equal" ~level:0 [(Tacentries.TyML (Tacentries.TyIdent ("f_equal", Tacentries.TyNil), (fun ist -> # 32 "plugins/cc/g_congruence.mlg" f_equal )))]