diff options
| author |  Jason Gross <jagro@google.com> | 2016-09-05 20:08:01 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-09-05 20:10:37 -0700 |
| commit | 29a462c0cb69af343e28b205628115354cd573ad (patch) | |
| tree | d71309c02d1c8ec677d03a504671163d6aaf6835 /src/Reflection/Reify.v | |
| parent | 235e58e2233a5c13a2065fdcd85073e016cad3df (diff) | |
Better implicits for Interp
Diffstat (limited to 'src/Reflection/Reify.v')
| -rw-r--r-- | src/Reflection/Reify.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Reflection/Reify.v b/src/Reflection/Reify.v index 1eac17675..58ebd5da5 100644 --- a/src/Reflection/Reify.v +++ b/src/Reflection/Reify.v @@ -226,7 +226,7 @@ Ltac rhs_of_goal := lazymatch goal with |- ?R ?LHS ?RHS => RHS end. Ltac Reify_rhs base_type_code interp_base_type op interp_op := let rhs := rhs_of_goal in let RHS := Reify base_type_code interp_base_type op rhs in - transitivity (Syntax.Interp base_type_code interp_base_type op interp_op RHS); + transitivity (Syntax.Interp interp_op RHS); [ | etransitivity; (* first we strip off the [InputSyntax.Compile] bit; Coq is bad at inferring the type, so we |