diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-03-28 19:21:00 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-03-28 19:21:00 -0400 |
| commit | 260dca24d6a1b517cd90932f4c57519e6bf8e0eb (patch) | |
| tree | 8dba71446fd55a66cb7a8e9024c3aff49ae88967 /src/Reflection/MapCastByDeBruijnWf.v | |
| parent | 2759b426f4b4ac6640e949f81568534923dd8d34 (diff) | |
Add Wf_MapCast to wf database
Diffstat (limited to 'src/Reflection/MapCastByDeBruijnWf.v')
| -rw-r--r-- | src/Reflection/MapCastByDeBruijnWf.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Reflection/MapCastByDeBruijnWf.v b/src/Reflection/MapCastByDeBruijnWf.v index 4bf5d7c29..eebd1330d 100644 --- a/src/Reflection/MapCastByDeBruijnWf.v +++ b/src/Reflection/MapCastByDeBruijnWf.v @@ -99,3 +99,5 @@ Section language. | intros ???; rewrite lookupb_empty by apply PositiveContextOk; congruence ]. Qed. End language. + +Hint Resolve Wf_MapCast : wf. |