diff options
author | 2016-10-29 22:52:35 -0400 | |
---|---|---|
committer | 2016-10-29 22:52:35 -0400 | |
commit | 4ae2f20dc35546bdc4e54a3570504778286cdd37 (patch) | |
tree | 86e68424738ef6c4f0af83963cca4a28105c5d52 /src | |
parent | 1c023b673a2fe06a97cc348494dd635bd965717c (diff) |
Fix type reification
Diffstat (limited to 'src')
-rw-r--r-- | src/Reflection/Reify.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Reflection/Reify.v b/src/Reflection/Reify.v index 341779099..b10ab66f4 100644 --- a/src/Reflection/Reify.v +++ b/src/Reflection/Reify.v @@ -35,7 +35,7 @@ Ltac reify_flat_type T := constr:(@Prod _ a b) | _ => let v := reify_base_type T in - constr:(Tbase v) + constr:(@Tbase _ v) end. Ltac reify_type T := lazymatch T with @@ -45,7 +45,7 @@ Ltac reify_type T := constr:(@Arrow _ a b) | _ => let v := reify_flat_type T in - constr:(Tflat v) + constr:(@Tflat _ v) end. Ltac reifyf_var x mkVar := |