diff options
| author |  Jason Gross <jgross@mit.edu> | 2019-03-08 00:54:23 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2019-03-08 00:54:23 -0500 |
| commit | aab9926b913e099ad2946acca5b8a01e642f40fc (patch) | |
| tree | f49b7e8481b7189e57292c734b127b57806af8cb /src | |
| parent | 960c26fe3c931b555e69240c639eaed8c378dd4b (diff) | |
Fix a typo
Diffstat (limited to 'src')
| -rw-r--r-- | src/LanguageWf.v | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/src/LanguageWf.v b/src/LanguageWf.v index 0e4822701..0ec717e70 100644 --- a/src/LanguageWf.v +++ b/src/LanguageWf.v @@ -1082,7 +1082,6 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [ Lemma wf_smart_Literal_eq {t v1 v2 G} : v1 = v2 -> expr.wf G (@ident.smart_Literal var1 t v1) (@ident.smart_Literal var2 t v2). Proof using Type. intro; subst; apply wf_smart_Literal. Qed. - Qed. End with_var2. Lemma Wf_Reify_as {t} v : expr.Wf (@GallinaReify.base.Reify_as t v). |