X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FProgrammingLanguage.v;h=b00d1ad035435638fe0080ab4930d539e8d9ae0c;hp=d1a0875a6d5b2a8108544d999e0dacf25b635572;hb=8cb97991a95d5761a28ca94767b8fe637d1411d9;hpb=97552c1a6dfb32098d4491951929ab1d4aca96a0

diff --git a/src/ProgrammingLanguage.v b/src/ProgrammingLanguage.v
index d1a0875..b00d1ad 100644
--- a/src/ProgrammingLanguage.v
+++ b/src/ProgrammingLanguage.v
@@ -248,11 +248,11 @@ Section Programming_Language.
       apply al_subst_associativity'.
       Defined.
 
-    Definition TypesLEnrichedInJudgments0 : Enrichment.
+    Definition TypesEnrichedInJudgments : Enrichment.
       refine {| enr_c := TypesLFC |}.
       Defined.
 
-    Definition TypesL_first c : EFunctor TypesLFC TypesLFC (fun x => x,,c ).
+    Definition Types_first c : EFunctor TypesLFC TypesLFC (fun x => x,,c ).
 (*
       eapply Build_EFunctor; intros.
       eapply MonoidalCat_all_central.
@@ -262,11 +262,11 @@ Section Programming_Language.
       admit.
       Defined.
 
-    Definition TypesL_second c : EFunctor TypesLFC TypesLFC (fun x => c,,x ).
+    Definition Types_second c : EFunctor TypesLFC TypesLFC (fun x => c,,x ).
       admit.
       Defined.
 
-    Definition TypesL_binoidal : BinoidalCat TypesLFC (@T_Branch _).
+    Definition Types_binoidal : BinoidalCat TypesLFC (@T_Branch _).
       refine
         {| bin_first  := TypesL_first
          ; bin_second := TypesL_second