From bdddd649c6cdd6196223d4574539ed819cbdc7a4 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 15 Jun 2020 12:45:40 +0200
Subject: [PATCH] Write constructors of `type` in a consistent way.

---
 theories/typing/interp.v |  5 ++---
 theories/typing/types.v  | 10 +++++-----
 2 files changed, 7 insertions(+), 8 deletions(-)

diff --git a/theories/typing/interp.v b/theories/typing/interp.v
index 7f52e37..6f78bac 100644
--- a/theories/typing/interp.v
+++ b/theories/typing/interp.v
@@ -96,7 +96,7 @@ Section interp_ren.
       { by rewrite !lookup_app_l. }
       change (bi_ofeO (uPredI (iResUR Σ))) with (uPredO (iResUR Σ)).
       rewrite !lookup_app_r; [|lia..].
-      assert ((length Δ1 + S (x - length Δ1) - length Δ1) = S (x - length Δ1)) as Hwat.
+      assert (∀ x, (length Δ1 + S (x - length Δ1) - length Δ1) = S (x - length Δ1)) as Hwat.
       { lia. }
       rewrite Hwat. simpl. done.
     - intros v1 v2; unfold lrel_car; simpl;
@@ -151,7 +151,7 @@ Section interp_ren.
       rewrite iter_up; case_decide; simpl; properness.
       { by rewrite !lookup_app_l. }
       rewrite !lookup_app_r; [|lia..].
-      case EQ: (x - length Δ1)=> [|n]; simpl.
+      case EQ: (_ - length Δ1)=> [|n]; simpl.
       { symmetry.
         pose (HW := interp_weaken [] Δ1 Δ2 τ' w1 w2).
         etrans; last by apply HW.
@@ -248,4 +248,3 @@ Notation "'{' Δ ';' Γ '}' ⊨ e '≤log≤' e' : τ" :=
   (at level 100, Δ at next level, Γ at next level, e, e' at next level,
    Ï„ at level 200,
    format "'[hv' '{' Δ ';'  Γ '}'  ⊨  '/  ' e  '/' '≤log≤'  '/  ' e'  :  τ ']'").
-
diff --git a/theories/typing/types.v b/theories/typing/types.v
index 9a7c675..ad16eb3 100644
--- a/theories/typing/types.v
+++ b/theories/typing/types.v
@@ -12,11 +12,11 @@ Inductive type :=
   | TProd : type → type → type
   | TSum : type → type → type
   | TArrow : type → type → type
-  | TRec (Ï„ : {bind 1 of type})
-  | TVar (x : var)
-  | TForall (Ï„ : {bind 1 of type})
-  | TExists (Ï„ : {bind 1 of type})
-  | Tref (Ï„ : type).
+  | TRec : {bind 1 of type} → type
+  | TVar : var → type
+  | TForall : {bind 1 of type} → type
+  | TExists : {bind 1 of type} → type
+  | Tref : type → type.
 
 (** Which types support equality testing *)
 Inductive EqType : type → Prop :=
-- 
GitLab