diff options
author | 2016-10-30 12:40:25 -0400 | |
---|---|---|
committer | 2016-10-30 12:40:25 -0400 | |
commit | dcff7c65666a13a95950adcd933ca162db32622c (patch) | |
tree | 4bd0c4f471dce9c55902b9152da384dd6d32a6da /src | |
parent | 8b2212fd3b9bf79ab48d30af61cc12c1dc700355 (diff) |
Adjust arguments to InputSyntax.Compile
Diffstat (limited to 'src')
-rw-r--r-- | src/Reflection/InputSyntax.v | 1 | ||||
-rw-r--r-- | src/Reflection/Reify.v | 2 |
2 files changed, 2 insertions, 1 deletions
diff --git a/src/Reflection/InputSyntax.v b/src/Reflection/InputSyntax.v index 1c97d2174..5d1500d20 100644 --- a/src/Reflection/InputSyntax.v +++ b/src/Reflection/InputSyntax.v @@ -134,3 +134,4 @@ Global Arguments MatchPair {_ _ _ _ _ _} _ {_} _. Global Arguments Pair {_ _ _ _ _} _ {_} _. Global Arguments Return {_ _ _ _ _} _. Global Arguments Abs {_ _ _ _ _ _} _. +Global Arguments Compile {_ _ _ t} _ _. diff --git a/src/Reflection/Reify.v b/src/Reflection/Reify.v index b55abd21b..fbe718f6c 100644 --- a/src/Reflection/Reify.v +++ b/src/Reflection/Reify.v @@ -235,7 +235,7 @@ Ltac Reify' base_type_code interp_base_type op e := end. Ltac Reify base_type_code interp_base_type op e := let r := Reify' base_type_code interp_base_type op e in - constr:(InputSyntax.Compile base_type_code interp_base_type op r). + constr:(@InputSyntax.Compile base_type_code interp_base_type op _ r). Ltac lhs_of_goal := lazymatch goal with |- ?R ?LHS ?RHS => LHS end. Ltac rhs_of_goal := lazymatch goal with |- ?R ?LHS ?RHS => RHS end. |