rename context to env

coq/_CoqProject

@@ -10,7 +10,7 @@ metatheory/Metatheory.v
 terms/debruijn.v
 terms/equiv.v
 terms/eval.v
-typing/context.v
+typing/env.v
 typing/subtype.v
 typing/morph.v
 typing/typing.v

coq/terms/eval.v

@@ -3,7 +3,6 @@ Import ListNotations.
 Require Import Atom.
 Require Import debruijn.
 Require Import subtype.
-Require Import context.
 Require Import morph.
 Require Import typing.
 

coq/typing/context.v

@@ -1,4 +0,0 @@
-Require Import Atom.
-Require Import debruijn.
-
-Definition context : Type := (list (atom * type_DeBruijn)).

coq/typing/env.v

@@ -0,0 +1,5 @@
+Require Import Atom.
+Require Import Environment.
+Require Import debruijn.
+
+Notation env := (list (atom * type_DeBruijn)).

coq/typing/morph.v

@@ -1,7 +1,7 @@
 Require Import debruijn.
 Require Import equiv.
 Require Import subtype.
-Require Import context.
+Require Import env.
 Require Import Atom.
 Import AtomImpl.
 From Coq Require Import Lists.List.
@@ -13,7 +13,7 @@ Open Scope ladder_expr_scope.
 (* Given a context, there is a morphism path from τ to τ' *)
 Reserved Notation "Γ '|-' σ '~~>' τ" (at level 101).
 
-Inductive morphism_path : context -> type_DeBruijn -> type_DeBruijn -> Prop :=
+Inductive morphism_path : env -> type_DeBruijn -> type_DeBruijn -> Prop :=
   | M_Sub : forall Γ τ τ',
     τ :<= τ' ->
     (Γ |- τ ~~> τ')
@@ -51,7 +51,7 @@ Reserved Notation "Γ '|-' '[[' σ '~~>' τ ']]' '=' m" (at level 101).
 (* some atom for the 'map' function on lists *)
 Parameter at_map : atom.
 
-Inductive translate_morphism_path : context -> type_DeBruijn -> type_DeBruijn -> expr_DeBruijn -> Prop :=
+Inductive translate_morphism_path : env -> type_DeBruijn -> type_DeBruijn -> expr_DeBruijn -> Prop :=
   | Translate_Descend : forall Γ τ τ',
     (τ :<= τ') ->
     (Γ |- [[ τ ~~> τ' ]] = [{ λ τ ↦morph (%0 des τ') }])

coq/typing/typing.v

@@ -4,14 +4,14 @@ Require Import Metatheory.
 Require Import Atom.
 Require Import debruijn.
 Require Import subtype.
-Require Import context.
+Require Import env.
 Require Import morph.
 
 Open Scope ladder_type_scope.
 Open Scope ladder_expr_scope.
 
 Reserved Notation "Γ '|-' x '\is' X"  (at level 101).
-Inductive typing : context -> expr_DeBruijn -> type_DeBruijn -> Prop :=
+Inductive typing : env -> expr_DeBruijn -> type_DeBruijn -> Prop :=
   | T_Var : forall Γ x τ,
     (In (x, τ) Γ) ->
     (Γ |- [{ $x }] \is τ)
@@ -70,7 +70,7 @@ where "Γ '|-' x '\is' τ" := (typing Γ x τ).
 
 Reserved Notation "Γ '|-' '[[' e \is τ ']]' '=' f"  (at level 101).
 
-Inductive translate_typing : context -> expr_DeBruijn -> type_DeBruijn -> expr_DeBruijn -> Prop :=
+Inductive translate_typing : env -> expr_DeBruijn -> type_DeBruijn -> expr_DeBruijn -> Prop :=
 
   | Expand_Var : forall Γ x τ,
     (Γ |- [{ $x }] \is τ) ->