Vous avez reçu un message "Your GitLab account has been locked ..." ? Pas d'inquiétude : lisez cet article https://docs.gricad-pages.univ-grenoble-alpes.fr/help/unlock/

Commit eca14936 authored by Xavier Leroy's avatar Xavier Leroy
Browse files

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.
parent ab62e1be
......@@ -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.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment