diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-03-30 17:33:29 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-03-30 17:33:29 -0400 |
| commit | 192119ee17576016b2bc35685cd0ce9bdec54c0a (patch) | |
| tree | 909b9a1cc8fe2c3a5d5b09cb5c2a0d833e2805f6 /src | |
| parent | 9a53f95941e069722978e6c23ced7e65ed6d457a (diff) | |
Reorder arguments to Wf_MapCast for eauto
This way we pick up the equality hypothesis first.
Diffstat (limited to 'src')
| -rw-r--r-- | src/Reflection/MapCastByDeBruijnWf.v | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/src/Reflection/MapCastByDeBruijnWf.v b/src/Reflection/MapCastByDeBruijnWf.v index 7130c00ea..fd8b824ca 100644 --- a/src/Reflection/MapCastByDeBruijnWf.v +++ b/src/Reflection/MapCastByDeBruijnWf.v @@ -69,9 +69,8 @@ Section language. Local Arguments Compile.compile : simpl never. Lemma Wf_MapCast {t} (e : Expr base_type_code op t) - (Hwf : Wf e) (input_bounds : interp_flat_type interp_base_type_bounds (domain t)) - : forall {b} e' (He':MapCast e input_bounds = Some (existT _ b e')), + : forall {b} e' (He':MapCast e input_bounds = Some (existT _ b e')) (Hwf : Wf e), Wf e'. Proof. unfold MapCastByDeBruijn.MapCast, MapCastCompile, MapCastDoCast, MapCastDoInterp, option_map; intros b e'. @@ -96,12 +95,12 @@ Section language. Lemma Wf_MapCast_arrow {s d} (e : Expr base_type_code op (Arrow s d)) - (Hwf : Wf e) (input_bounds : interp_flat_type interp_base_type_bounds s) : forall {b} (e' : Expr _ _ (Arrow (pick_type input_bounds) (pick_type b))) - (He':MapCast e input_bounds = Some (existT _ b e')), + (He':MapCast e input_bounds = Some (existT _ b e')) + (Hwf : Wf e), Wf e'. - Proof. exact (@Wf_MapCast (Arrow s d) e Hwf input_bounds). Qed. + Proof. exact (@Wf_MapCast (Arrow s d) e input_bounds). Qed. End language. Hint Resolve Wf_MapCast Wf_MapCast_arrow : wf. |