From d6195d3cf5fb38b917e68fda16655aa43bd1dc51 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9o=20Winterhalter?= <theo.winterhalter@gmail.com>
Date: Sat, 27 Jul 2024 13:14:55 +0200
Subject: [PATCH] Fix import in unscoped

---
 theories/autosubst/Makefile   | 4 ++--
 theories/autosubst/unscoped.v | 6 +++---
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/theories/autosubst/Makefile b/theories/autosubst/Makefile
index 990c111..3a3ef7f 100644
--- a/theories/autosubst/Makefile
+++ b/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
diff --git a/theories/autosubst/unscoped.v b/theories/autosubst/unscoped.v
index 55f8172..c5d2d98 100644
--- a/theories/autosubst/unscoped.v
+++ b/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.
\ No newline at end of file
+                        end.