clean up

Author: MevenBertrand

_CoqProject

@@ -71,7 +71,6 @@ theories/Fundamental.v
 
 theories/AlgorithmicTyping.v
 theories/Algorithmic/UntypedAlgorithmicConversion.v
-theories/Algorithmic/PremisePreserve.v
 theories/Algorithmic/BundledAlgorithmicTyping.v
 theories/Algorithmic/AlgorithmicConvProperties.v
 theories/Algorithmic/AlgorithmicTypingProperties.v

theories/Algorithmic/PremisePreserve.v

@@ -1,11 +1,5 @@
 (** * LogRel.UntypedAlgorithmicConversion: alternative definition of algorithmic conversion. *)
 
-From LogRel Require Import PremisePreserve.
-From MetaCoq.Utils Require Import bytestring.
-From MetaCoq.Template Require Import Loader.
-
-Open Scope bs.
-
 From LogRel Require Import Utils Syntax.All GenericTyping DeclarativeTyping AlgorithmicTyping.
 From LogRel Require Import Sections.
 From LogRel.TypingProperties Require Import PropertiesDefinition DeclarativeProperties SubstConsequences TypeConstructorsInj NeutralConvProperties.

theories/Algorithmic/UntypedAlgorithmicConversion.v

@@ -1,14 +1,9 @@
 (** * LogRel.Decidability.UntypedCompleteness: the inductive predicates imply the implementation answer positively. *)
 From Coq Require Import Nat Lia Arith.
 From Equations Require Import Equations.
-From LogRel Require Import Syntax.All DeclarativeTyping GenericTyping AlgorithmicTyping.
+From LogRel Require Import Utils Syntax.All DeclarativeTyping GenericTyping AlgorithmicTyping.
 From LogRel.TypingProperties Require Import DeclarativeProperties PropertiesDefinition SubstConsequences TypeConstructorsInj NeutralConvProperties.
 From LogRel.Algorithmic Require Import BundledAlgorithmicTyping AlgorithmicConvProperties AlgorithmicTypingProperties UntypedAlgorithmicConversion.
-
-(* To get the right easy tactic, should be fixed otherwise *)
-From LogRel Require Import Utils.
-Check fixme.
-
 From LogRel.Decidability Require Import Functions UntypedFunctions Soundness UntypedSoundness Completeness.
 From PartialFun Require Import Monad PartialFun MonadExn.