Fix import in unscoped

theories/autosubst/Makefile

@@ -1,3 +1,3 @@
 syntax:
-	autosubst -f -s ucoq -v ge813 -allfv GAST.sig -o GAST.v -p AST_preamble
-	autosubst -f -s ucoq -v ge813 -allfv CCAST.sig -o CCAST.v -p AST_preamble
+	autosubst -no-static -f -s ucoq -v ge813 -allfv GAST.sig -o GAST.v -p AST_preamble
+	autosubst -no-static -f -s ucoq -v ge813 -allfv CCAST.sig -o CCAST.v -p AST_preamble

theories/autosubst/unscoped.v

@@ -7,7 +7,7 @@ Version: December 11, 2019.
  I changed this library a bit to work better with my generated code.
  1. I use nat directly instead of defining fin to be nat and using Some/None as S/O
  2. I removed the "s, sigma" notation for scons because it interacts with dependent function types "forall x, A"*)
-Require Import core.
+From GhostTT.autosubst Require Import core.
 Require Import Setoid Morphisms Relation_Definitions.
 
 Definition ap {X Y} (f : X -> Y) {x y : X} (p : x = y) : f x = f y :=
@@ -170,7 +170,7 @@ Module UnscopedNotations.
   Include RenNotations.
   Include SubstNotations.
   Include CombineNotations.
-  
+
   (* Notation "s , sigma" := (scons s sigma) (at level 60, format "s ,  sigma", right associativity) : subst_scope. *)
 
   Notation "s '..'" := (scons s ids) (at level 1, format "s ..") : subst_scope.
@@ -210,4 +210,4 @@ Ltac fsimpl :=
          (* DONE had to put an underscore as the last argument to scons. This might be an argument against unfolding funcomp *)
          | [|- context[funcomp _ (scons _ _)]] => setoid_rewrite scons_comp'; eta_reduce
          | [|- context[scons var_zero shift]] => setoid_rewrite scons_eta_id'; eta_reduce
-                        end.
+                        end.