diff options
| author | coqbot-app[bot] | 2020-11-05 15:32:31 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-05 15:32:31 +0000 |
| commit | afc828b3e207dd39c59d1501d570a88b2012fd2c (patch) | |
| tree | f9af32a8b25439a9eb6c8407f99ad94f78a64fda /Makefile.common | |
| parent | b95c38d3d28a59da7ff7474ece0cb42623497b7d (diff) | |
| parent | e6f7517be65e9f5d2127a86e2213eb717d37e43f (diff) | |
Merge PR #12218: Numeral notations for non inductive types
Reviewed-by: herbelin
Reviewed-by: JasonGross
Reviewed-by: jfehrle
Ack-by: Zimmi48
Diffstat (limited to 'Makefile.common')
| -rw-r--r-- | Makefile.common | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/Makefile.common b/Makefile.common index a482b9b963..caf1821ce5 100644 --- a/Makefile.common +++ b/Makefile.common @@ -149,11 +149,9 @@ CCCMO:=plugins/cc/cc_plugin.cmo BTAUTOCMO:=plugins/btauto/btauto_plugin.cmo RTAUTOCMO:=plugins/rtauto/rtauto_plugin.cmo SYNTAXCMO:=$(addprefix plugins/syntax/, \ - r_syntax_plugin.cmo \ int63_syntax_plugin.cmo \ float_syntax_plugin.cmo \ - numeral_notation_plugin.cmo \ - string_notation_plugin.cmo) + number_string_notation_plugin.cmo) DERIVECMO:=plugins/derive/derive_plugin.cmo LTACCMO:=plugins/ltac/ltac_plugin.cmo plugins/ltac/tauto_plugin.cmo SSRMATCHINGCMO:=plugins/ssrmatching/ssrmatching_plugin.cmo |