summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--grammars/logic/Logic.gf2
1 files changed, 1 insertions, 1 deletions
diff --git a/grammars/logic/Logic.gf b/grammars/logic/Logic.gf
index 334592946..3e2516ebc 100644
--- a/grammars/logic/Logic.gf
+++ b/grammars/logic/Logic.gf
@@ -27,7 +27,7 @@ fun
Univ : (A : Dom) -> (Elem A -> Prop) -> Prop ;
Exist : (A : Dom) -> (Elem A -> Prop) -> Prop ;
-
+
-- progressive implication à la type theory
ImplP : (A : Prop) -> (Proof A -> Prop) -> Prop ;