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 | |
| parent | 235e58e2233a5c13a2065fdcd85073e016cad3df (diff) | |
Better implicits for Interp
| -rw-r--r-- | src/Reflection/InputSyntax.v | 2 | ||||
| -rw-r--r-- | src/Reflection/Reify.v | 2 | ||||
| -rw-r--r-- | src/Reflection/Syntax.v | 1 |
3 files changed, 3 insertions, 2 deletions
diff --git a/src/Reflection/InputSyntax.v b/src/Reflection/InputSyntax.v index c3c796d75..98faeaa44 100644 --- a/src/Reflection/InputSyntax.v +++ b/src/Reflection/InputSyntax.v @@ -105,7 +105,7 @@ Section language. Qed. Lemma Compile_correct {t : flat_type} (e : @Expr t) - : Syntax.Interp base_type_code interp_base_type op interp_op (Compile e) = Interp interp_op e. + : Syntax.Interp interp_op (Compile e) = Interp interp_op e. Proof. unfold Interp, Compile, Syntax.Interp; simpl. pose (e (interp_flat_type_gen interp_base_type)) as E. 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 diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v index f1ff5afe2..ae4cbb6e2 100644 --- a/src/Reflection/Syntax.v +++ b/src/Reflection/Syntax.v @@ -205,6 +205,7 @@ Global Arguments interp_type {_} _ _. Global Arguments wff {_ _ _ _ _} G {t} _ _. Global Arguments wf {_ _ _ _ _} G {t} _ _. Global Arguments Wf {_ _ _ t} _. +Global Arguments Interp {_ _ _} interp_op {t} _. Notation "'slet' x := A 'in' b" := (Let A (fun x => b)) : expr_scope. Notation "'λ' x .. y , t" := (Abs (fun x => .. (Abs (fun y => t%expr)) ..)) : expr_scope. |