diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-29 22:52:35 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-29 22:52:35 -0400 |
| commit | 4ae2f20dc35546bdc4e54a3570504778286cdd37 (patch) | |
| tree | 86e68424738ef6c4f0af83963cca4a28105c5d52 /src/Reflection/Reify.v | |
| parent | 1c023b673a2fe06a97cc348494dd635bd965717c (diff) | |
Fix type reification
Diffstat (limited to 'src/Reflection/Reify.v')
| -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 := |