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 ;