Rm lowlang (1)

flake.nix

@@ -208,6 +208,17 @@
                 packages = [minuska minuska.coqPackages.coq-lsp minuska.coqPackages.coq];
               };
 
+          languages-in-coq =
+            let
+              languages-in-coq = self.outputs.packages.${system}.languages-in-coq;
+            in
+              pkgs.mkShell {
+                inputsFrom = [languages-in-coq];
+                packages = [
+                  languages-in-coq.coqPackages.coq-lsp
+                ];
+              };
+
           examples-coq =
             let
               examples-coq = self.outputs.packages.${system}.examples-coq;

languages-in-coq/theories/examples.v

@@ -802,9 +802,7 @@ Module imp.
         (naive_interpreter Γ.1) 
     .
     Proof.
-        Check @naive_interpreter_sound.
-        apply @naive_interpreter_sound.
-        { apply _. }
+        apply naive_interpreter_sound.
         ltac1:(assert(Htmp: isSome(RewritingTheory2_wf_heuristics (Γ.1)))).
         {
             ltac1:(compute_done).

minuska/_CoqProject

@@ -9,8 +9,8 @@ theories/spec_syntax.v
 theories/varsof.v
 theories/syntax_properties.v
 theories/semantics_properties.v
-theories/spec_lowlang_interpreter.v
 theories/spec_interpreter.v
+theories/valuation_merge.v
 
 theories/minuska.v
 theories/string_variables.v

minuska/bin/main.ml

@@ -36,7 +36,7 @@ let append_definition input_filename output_channel =
     .
     Proof.
         apply @global_naive_interpreter_sound.
-        { apply _. }
+        (*{ apply _. }*)
         ltac1:(assert(Htmp: isSome(RewritingTheory2_wf_heuristics (fst T)))).
         {
             apply language_well_formed.