aboutsummaryrefslogtreecommitdiff
path: root/proofs/clenvtac.mli
AgeCommit message (Expand)Author
2012-08-08Updating headers.herbelin
2012-05-29remove many excessive open Util & Errors in mli'sletouzey
2012-03-02Noise for nothingpboutill
2011-06-10Moved allow_K to a unification flagherbelin
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2008-12-14Fix looping class resolution bug discovered by B. Aydemir and use themsozeau
2008-06-21- Implantation de la suggestion 1873 sur discriminate. Au final,herbelin
2008-04-13Bugs, nettoyage, et améliorations diversesherbelin
2008-02-13Essai de prise en compte de delta dans unify_0 (même sur termes non clos). herbelin
2007-10-03Ajout de eelim, ecase, edestruct et einduction (expérimental).herbelin
2004-09-12inclusion de meta_map dans evar_defsbarras
2004-09-10simplification de clenvbarras
2004-09-07deuxieme vague de modifs: evar_defs fonctionnelbarras
2004-09-03premiere reorganisation de l\'unificationbarras
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-22 07:42:09 +0000