cleaning up structuration

CoqHott · Jan 4, 2024 · 447c8c7 · 447c8c7
1 parent 28e1b98
commit 447c8c7
Show file tree

Hide file tree

Showing 3 changed files with 0 additions and 2 deletions.
diff --git a/docs/dependency_graph.png b/docs/dependency_graph.png
diff --git a/theories/BasicAst.v b/theories/BasicAst.v
@@ -1,6 +1,5 @@
 (** * LogRel.BasicAst: definitions preceding those of the AST of terms: sorts, binder annotations… *)
 From Coq Require Import String Bool.
-From LogRel.AutoSubst Require Import core unscoped.
 
 Inductive sort :=
   | set : sort.

diff --git a/theories/Utils.v b/theories/Utils.v
@@ -2,7 +2,6 @@
 From Coq Require Import Morphisms List CRelationClasses.
 From Coq Require Import ssrbool.
 From smpl Require Import Smpl.
-From LogRel.AutoSubst Require Import core unscoped Ast.
 
 Set Universe Polymorphism.
 Set Polymorphic Inductive Cumulativity.