diff options
Diffstat (limited to 'test-suite/complexity')
| -rw-r--r-- | test-suite/complexity/injection.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/test-suite/complexity/injection.v b/test-suite/complexity/injection.v index db2d9c53f..335996c27 100644 --- a/test-suite/complexity/injection.v +++ b/test-suite/complexity/injection.v @@ -43,11 +43,11 @@ Record joinmap (key: Type) (t: Type) (j : joinable t) : Type exists s2, jm_j.(join) s1 s2 s3 }. -Parameter mkJoinmap : forall (key: Type) (t: Type) (j: joinable t), +Parameter mkJoinmap : forall (key: Type) (t: Type) (j: joinable t), joinmap key j. Parameter ADMIT: forall p: Prop, p. -Implicit Arguments ADMIT [p]. +Implicit Arguments ADMIT [p]. Module Share. Parameter jb : joinable bool. @@ -90,7 +90,7 @@ Definition jown : joinable own := Joinable own_is_empty own_join ADMIT ADMIT ADMIT ADMIT ADMIT ADMIT ADMIT ADMIT . End Own. - + Fixpoint sinv (n: nat) : Type := match n with | O => unit |