diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-30 12:37:28 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-30 12:37:28 -0400 |
| commit | 8b2212fd3b9bf79ab48d30af61cc12c1dc700355 (patch) | |
| tree | 1d8fc8fc9402f4d7aec00321150d93b95def3ae4 /src/Reflection/Reify.v | |
| parent | 7a9faafa8a3507bc20ae15bbe71200d9c4b5a12b (diff) | |
Generalize Reify a bit
Diffstat (limited to 'src/Reflection/Reify.v')
| -rw-r--r-- | src/Reflection/Reify.v | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/Reflection/Reify.v b/src/Reflection/Reify.v index 7ad4f42c1..b55abd21b 100644 --- a/src/Reflection/Reify.v +++ b/src/Reflection/Reify.v @@ -247,7 +247,13 @@ Ltac Reify_rhs_gen Reify prove_interp_compile_correct interp_op try_tac := transitivity (Syntax.Interp interp_op RHS'); [ | transitivity (Syntax.Interp interp_op RHS); - [ apply f_equal; vm_compute; reflexivity + [ lazymatch goal with + | [ |- ?R ?x ?y ] + => cut (x = y) + end; + [ let H := fresh in + intro H; rewrite H; reflexivity + | apply f_equal; vm_compute; reflexivity ] | etransitivity; (* first we strip off the [InputSyntax.Compile] bit; Coq is bad at inferring the type, so we help it out by providing it *) |