diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-01-21 16:07:24 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-01-21 16:07:24 +0100 |
| commit | eca149363d20d94198a4b1e1ae4f9f964e468098 (patch) | |
| tree | 5b8573ab8114b5aabd308aa65e834934c1961b94 /lib | |
| parent | ab62e1bed37d2efe4d2a9e0139839bae21b1cdd9 (diff) | |
| download | compcert-kvx-eca149363d20d94198a4b1e1ae4f9f964e468098.tar.gz compcert-kvx-eca149363d20d94198a4b1e1ae4f9f964e468098.zip | |
Define `fold_ind_aux` and `fold_ind` transparently
The extraction mechanism wants to extract them (because they are in
Type, probably). The current opaque definition causes a warning at
extraction-time.
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/Maps.v | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -1349,7 +1349,7 @@ Proof. + inv NOREPET. auto. + apply FINAL. auto. + apply IHl. auto. inv NOREPET; auto. -Qed. +Defined. Theorem fold_ind: P m_final (T.fold f m_final init). @@ -1364,7 +1364,7 @@ Proof. rewrite T.fold_spec. apply X. intros; simpl. rewrite <- List.in_rev. split. apply T.elements_complete. apply T.elements_correct. -Qed. +Defined. End TREE_FOLD_IND. |