diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-03-14 15:15:22 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-03-14 15:15:22 -0400 |
| commit | 4bac3c49dba1e261a1afcc600c11b54673afd99c (patch) | |
| tree | c061c573d96ac93abe87bd3b5ed600327ca76126 /src/Reflection/Named | |
| parent | bf3783de77c05bd3e43ac7e2d2f1f3375bd5f09e (diff) | |
Remove useless hyps
Diffstat (limited to 'src/Reflection/Named')
| -rw-r--r-- | src/Reflection/Named/InterpretToPHOAS.v | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/src/Reflection/Named/InterpretToPHOAS.v b/src/Reflection/Named/InterpretToPHOAS.v index 94cab3b87..4b3ef1b84 100644 --- a/src/Reflection/Named/InterpretToPHOAS.v +++ b/src/Reflection/Named/InterpretToPHOAS.v @@ -8,8 +8,6 @@ Module Export Named. Context {base_type_code : Type} {op : flat_type base_type_code -> flat_type base_type_code -> Type} {var : base_type_code -> Type} - (base_type_code_beq : base_type_code -> base_type_code -> bool) - (base_type_code_bl_transparent : forall x y, base_type_code_beq x y = true -> x = y) {Name} {Context : Context Name var}. |