diff options
| author |  Jason Gross <jgross@mit.edu> | 2019-03-31 10:04:22 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2019-03-31 10:04:22 -0400 |
| commit | bcc7a5f7d3a15c2e8770a530ed3fa0ec45b60725 (patch) | |
| tree | 1b8122dd5a21914c84e2e3eb2f5d8e0be6b2ad70 /src | |
| parent | 25761f294d165487bec8832272c58dae82038b95 (diff) | |
Fix a non-terminated comment
Diffstat (limited to 'src')
| -rw-r--r-- | src/Rewriter.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Rewriter.v b/src/Rewriter.v index 99201e27d..3ca65c2bf 100644 --- a/src/Rewriter.v +++ b/src/Rewriter.v @@ -1297,7 +1297,7 @@ Module Compilers. "evaluated" in Gallina (e.g., [eager_list_rect] turns into [list_rect] over a concrete list of cons cells holding PHOAS expressions), and the result of this evaluation is - returned." *) + returned. *) (* N.B. the [with_lets] argument to [reflect] doesn't matter here because [value' true (_ → _) ≡ value' false (_ → _)] *) Definition reflect_ident_iota {t} (idc : ident t) : option (value t) |