diff options
| author |  Jason Gross <jagro@google.com> | 2018-08-02 16:24:58 -0400 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2018-08-02 16:24:58 -0400 |
| commit | 3b910ee76354cd9aadb8cf53f0e5c490ca73d1ec (patch) | |
| tree | e04f52423780ee5b2efb84f8e2e350ded33dc3b1 /src/Experiments/NewPipeline/Rewriter.v | |
| parent | 132b663247c195a38385f8b9f473b998f2e2d37b (diff) | |
Make ERROR_BAD_REWRITE_RULE Opaque, not Qed'ed
This allows us to prove things on the basis of it being the identity
function, which we need to do to prove well-formedness without being
able to compute the natural types of rewrite rules (which will be coming
later).
Diffstat (limited to 'src/Experiments/NewPipeline/Rewriter.v')
| -rw-r--r-- | src/Experiments/NewPipeline/Rewriter.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/Experiments/NewPipeline/Rewriter.v b/src/Experiments/NewPipeline/Rewriter.v index 5ebf429a1..313dd62e7 100644 --- a/src/Experiments/NewPipeline/Rewriter.v +++ b/src/Experiments/NewPipeline/Rewriter.v @@ -502,7 +502,8 @@ Module Compilers. Definition rewrite_rulesT := (list rewrite_ruleT). - Definition ERROR_BAD_REWRITE_RULE {t} (pat : pattern) (value : expr t) : expr t. exact value. Qed. + Definition ERROR_BAD_REWRITE_RULE {t} (pat : pattern) (value : expr t) : expr t := value. + Global Opaque ERROR_BAD_REWRITE_RULE. Definition eval_rewrite_rules (do_again : forall t : base.type, @expr.expr base.type ident value t -> UnderLets (expr t)) |