diff options
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 11 |
1 files changed, 6 insertions, 5 deletions
@@ -293,16 +293,17 @@ CCCMO=contrib/cc/ccalgo.cmo contrib/cc/ccproof.cmo contrib/cc/cctac.cmo \ contrib/cc/g_congruence.cmo SUBTACCMO=\ - contrib/subtac/scoq.cmo \ + contrib/subtac/subtac_utils.cmo \ contrib/subtac/eterm.cmo \ + contrib/subtac/g_eterm.cmo \ contrib/subtac/context.cmo \ contrib/subtac/subtac_errors.cmo \ contrib/subtac/subtac_coercion.cmo \ - contrib/subtac/interp.cmo \ - contrib/subtac/interp_fixpoint.cmo \ + contrib/subtac/subtac_pretyping.cmo \ + contrib/subtac/subtac_interp_fixpoint.cmo \ contrib/subtac/subtac_command.cmo \ contrib/subtac/subtac.cmo \ - contrib/subtac/sparser.cmo + contrib/subtac/g_subtac.cmo RTAUTOCMO=contrib/rtauto/proof_search.cmo contrib/rtauto/refl_tauto.cmo \ @@ -310,7 +311,7 @@ RTAUTOCMO=contrib/rtauto/proof_search.cmo contrib/rtauto/refl_tauto.cmo \ ML4FILES += contrib/jprover/jprover.ml4 contrib/cc/g_congruence.ml4 \ contrib/funind/tacinv.ml4 contrib/first-order/g_ground.ml4 \ - contrib/subtac/sparser.ml4 contrib/subtac/g_eterm.ml4 \ + contrib/subtac/g_subtac.ml4 contrib/subtac/g_eterm.ml4 \ contrib/rtauto/g_rtauto.ml4 contrib/recdef/recdef.ml4 \ contrib/funind/indfun_main.ml4 |