diff options
| -rw-r--r-- | src/Reflection/Syntax.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v index 2a6cce891..f9be9f318 100644 --- a/src/Reflection/Syntax.v +++ b/src/Reflection/Syntax.v @@ -421,6 +421,12 @@ Global Arguments Tbase {_}%type_scope _%ctype_scope. Ltac admit_Wf := apply Wf_admitted. +Fixpoint flatten_flat_type {base_type_code} (t : flat_type (flat_type base_type_code)) : flat_type base_type_code + := match t with + | Tbase T => T + | Prod A B => Prod (@flatten_flat_type _ A) (@flatten_flat_type _ B) + end. + Scheme Equality for flat_type. Scheme Equality for type. |