Fix minor stuffs in test-suite and translations

test-suite/_CoqProject

@@ -9,6 +9,8 @@
 -Q ../erasure/theories MetaCoq.Erasure
 -R . MetaCoq.TestSuite
 
+# list obtained with `ls -1 *.v`
+
 bug1.v
 bug2.v
 bug5.v
@@ -20,19 +22,23 @@ case.v
 castprop.v
 # CheckerTest.v disabled
 cofix.v
+erasure_live_test.v
+erasure_test.v
 evars.v
+extractable.v
 hnf_ctor.v
+issue27.v
+issue28.v
 letin.v
 mutind.v
 opaque.v
 proj.v
+run_in_tactic.v
+safechecker_test.v
+# test_term.v -> loaded in TypingTests.v
+tmExistingInstance.v
+tmInferInstance.v
 TypingTests.v
+unfold.v
 univ.v
-tmInferInstance.v
-issue27.v
-issue28.v
-extractable.v
 vs.v
-erasure_test.v
-safechecker_test.v
-erasure_live_test.v

test-suite/unfold.v

@@ -1,3 +1,3 @@
-Require Import MetaCoq.Template.All.
+Require Import MetaCoq.Template.All String.
 
 Run TemplateProgram (tmBind (tmEval (unfold "negb") negb) tmPrint).

translations/_CoqProject.in

@@ -6,7 +6,7 @@ sigma.v
 MiniHoTT.v
 MiniHoTT_paths.v
 translation_utils.v
-#param_original.v
+param_original.v
 param_cheap_packed.v
 param_generous_packed.v
 #param_generous_unpacked.v

translations/param_original.v

@@ -246,7 +246,6 @@ Module Id2.
   Definition free_thm_myf : forall A x y p, myf A x y p = p
     := param_ID_identity myf myfᵗ.
 End Id2.
-*)
 
 
 

translations/translation_utils.v

@@ -184,12 +184,6 @@ Definition Implement {tsl : Translation} (ΣE : tsl_context)
   end
   end.
 
-Definition body_constant_entry (e : constant_entry) : option term :=
-  match e with
-  | ParameterEntry _ => None
-  | DefinitionEntry {| definition_entry_body := t |} => Some t
-  end.
-
 
 Definition ImplementExisting {tsl : Translation} (ΣE : tsl_context) (id : ident)
   : TemplateMonad tsl_context :=