Commit 042bac41 authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

Natded: nettoyage des require

parent af2b6779
(** Alternative definitions of substs and alpha for named formulas *)
Require Import Morphisms RelationClasses Arith Omega Defs NameProofs Nam.
Require Import Defs NameProofs Nam.
Import ListNotations.
Import Nam.Form.
Import Nam.Form.Alt.
......
(** Equivalence between various substs and alpha for named formulas *)
Require Import Morphisms RelationClasses Arith Omega.
Require Import Defs NameProofs Nam Alpha Meta Equiv.
Import ListNotations.
Import Nam.Form.
......
Require Import Ascii NArith Omega Setoid Morphisms.
Require Import Defs Mix NameProofs Meta.
Require Import Ascii NArith Defs Mix NameProofs Meta.
Import ListNotations.
Local Open Scope bool_scope.
Local Open Scope lazy_bool_scope.
......
Require Export Arith Bool String MSetRBT StringOrder List Utils.
Require Export Setoid Morphisms RelationClasses Arith Omega Bool String
MSetRBT StringOrder List Utils.
Require DecimalString.
Import ListNotations.
Local Open Scope bool_scope.
......
(** Conversion from Named formulas to Locally Nameless formulas *)
Require Import RelationClasses Arith Omega Defs NameProofs.
Require Import Defs NameProofs.
Require Nam Mix.
Import ListNotations.
Import Nam Nam.Form.
......
(** Some Meta-properties (proved on the Mix encoding) *)
Require Import RelationClasses Arith Omega Defs NameProofs Mix.
Require Import Defs NameProofs Mix.
Import ListNotations.
Local Open Scope bool_scope.
Local Open Scope lazy_bool_scope.
......
Require Import Defs Mix NameProofs Meta Omega Setoid Morphisms
Eqdep_dec Theories PreModels.
Require Import Eqdep_dec Defs Mix NameProofs Meta Theories PreModels.
Import ListNotations.
Local Open Scope bool_scope.
Local Open Scope lazy_bool_scope.
......
Require Import Ascii Omega MSetFacts MSetProperties
Setoid Utils StringUtils Defs.
Require Import Ascii MSetFacts MSetProperties StringUtils Defs.
Local Open Scope bool_scope.
Local Open Scope lazy_bool_scope.
Local Open Scope string_scope.
......
Require Import Defs Mix NameProofs Meta Omega Setoid Morphisms.
Require Import Defs Mix NameProofs Meta.
Import ListNotations.
Local Open Scope bool_scope.
Local Open Scope lazy_bool_scope.
......
(** Notion of 1st order theories *)
Require Import Arith Omega Defs NameProofs Mix Meta Countable.
Require Import Coq.Program.Equality.
Require Import Defs NameProofs Mix Meta Countable.
Import ListNotations.
Local Open Scope bool_scope.
Local Open Scope eqb_scope.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment