proofs that Types/Judgments form an enrichment

[coq-hetmet.git] / src / NaturalDeduction.v

diff --git a/src/NaturalDeduction.v b/src/NaturalDeduction.v
index 2bc361f..407948b 100644 (file)
--- a/src/NaturalDeduction.v
+++ b/src/NaturalDeduction.v
@@ -1,5 +1,8 @@
 (*********************************************************************************************************************************)
-(* NaturalDeduction: structurally explicit proofs in Coq                                                                         *)
+(* NaturalDeduction:                                                                                                             *)
+(*                                                                                                                               *)
+(*   Structurally explicit natural deduction proofs.                                                                             *)
+(*                                                                                                                               *)
 (*********************************************************************************************************************************)
 
 Generalizable All Variables.