Move some 'evaluate logic in ML' files to new directory.

This code isn't being used and doesn't have any automatic test-cases, making it a real candidate for removal. However, for the moment, I'm just shifting it into a directory of its own (rather than having it in the unrelated src/datatype).
HOL-Theorem-Prover · Oct 22, 2014 · f5a6c58 · f5a6c58
1 parent 91e46ef
commit f5a6c58
Show file tree

Hide file tree

Showing 7 changed files with 1 addition and 0 deletions.
diff --git a/src/datatype/EvalRef.sig → src/boss/ml_evaluation/EvalRef.sig b/src/datatype/EvalRef.sig → src/boss/ml_evaluation/EvalRef.sig
diff --git a/src/datatype/EvalRef.sml → src/boss/ml_evaluation/EvalRef.sml b/src/datatype/EvalRef.sml → src/boss/ml_evaluation/EvalRef.sml
diff --git a/src/datatype/Interactive → src/boss/ml_evaluation/Interactive b/src/datatype/Interactive → src/boss/ml_evaluation/Interactive
diff --git a/src/datatype/Interactive.tests → src/boss/ml_evaluation/Interactive.tests b/src/datatype/Interactive.tests → src/boss/ml_evaluation/Interactive.tests
diff --git a/src/datatype/Lift.sig → src/boss/ml_evaluation/Lift.sig b/src/datatype/Lift.sig → src/boss/ml_evaluation/Lift.sig
diff --git a/src/datatype/Lift.sml → src/boss/ml_evaluation/Lift.sml b/src/datatype/Lift.sml → src/boss/ml_evaluation/Lift.sml
diff --git a/tools/sequences/core-theories b/tools/sequences/core-theories
@@ -39,6 +39,7 @@ src/monad
 src/quantHeuristics
 src/unwind
 src/HolSat/vector_def_CNF
+src/boss/ml_evaluation
 src/boss
 # Up to this point is needed for hol (which loads bossLib).
 # (Maybe unwind could be omitted).