aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/environ.ml
Commit message (Expand)AuthorAge
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* - Addition of "Hint Resolve ->" and "Hint Resolve <-" continued: itGravatar herbelin2009-05-10
* Some dead code removal + cleanupsGravatar letouzey2009-04-08
* Optionally list opaque constants in addition to axions/variables inGravatar msozeau2009-03-09
* Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->Gravatar herbelin2008-12-31
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* Correction du problème de complexité de Print Assumptions :Gravatar aspiwack2008-05-27
* Ajout des alias de module dans le noyau.Gravatar soubiran2008-03-14
* Merge with lmamane's private branch:Gravatar lmamane2008-02-22
* Beaoucoup de changements dans la representation interne des modules.Gravatar soubiran2008-02-01
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
* Nettoyage de Print Assumptions :Gravatar aspiwack2007-11-09
* Suppression des type_app et body_of_type qui alourdissent inutilement le codeGravatar herbelin2007-08-27
* kill an ugly warning about a non-exhaustive patternGravatar letouzey2007-06-26
* ajout de head0 et tail0 en natifGravatar bgregoir2007-06-20
* Corrections dans le Print Assumption. Les definitions locales ("Let") Gravatar aspiwack2007-05-30
* Processor integers + Print assumption (see coqdev mailing list for the Gravatar aspiwack2007-05-11
* Modification de la vm:Gravatar notin2007-03-27
* Suppression de code mortGravatar notin2007-02-01
* Correction du bug #1315:Gravatar notin2007-01-22
* Changement de comportement du [rewrite ... in H]: Coq échoue si HGravatar notin2006-10-03
* correction bugs de condition de garde (fix + cofix)Gravatar barras2006-05-12
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
* Détection var inutile par ocaml 3.09Gravatar herbelin2006-01-10
* changement d'egalite pour le named_context_valGravatar gregoire2005-12-05
* Changement des named_contextGravatar gregoire2005-12-02
* compatibility with POWERPCGravatar gregoire2004-11-22
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
* Changement dans les boxed values .Gravatar gregoire2004-11-12
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* Nouvelle en-têteGravatar herbelin2004-07-16
* bug #266 (Search Error si on calcule apres avoir fait Clear d'une var Local)Gravatar barras2003-12-16
* Suppression StronglyClassical, StronglyConstructive devient plus concretement...Gravatar herbelin2003-11-08
* Set devient predicatif par defautGravatar herbelin2003-10-28
* Contexte locale non-vide interdit a la fin d'un module ou module typeGravatar coq2002-12-18
* Lazy manuelles dans le codeGravatar coq2002-10-07
* Lazy experimentale temporaire...Gravatar coq2002-10-05
* RenoncementGravatar herbelin2002-08-13
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* resolution du pb d'efficacite du a Sign.add_named_declGravatar barras2002-04-04
* suppression de pop_namedGravatar barras2002-02-22
* petits changements cosmetiques sur les tactiquesGravatar barras2002-02-15
* - Reforme de la gestion des args recursifs (via arbres reguliers)Gravatar barras2002-02-14
* evaluable_constant retournait vrai pour les constantes opaques, ce qui faisaitGravatar barras2002-02-05
* compat ocaml 3.03Gravatar filliatr2001-12-13
* types vs constrGravatar herbelin2001-11-20
* Suites modifs du noyau. Univ devient purement fonctionnel.Gravatar barras2001-11-12
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 17:31:38 +0000