index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
Makefile
Commit message (
Expand
)
Author
Age
*
Abandon gestion des extensions de syntaxe de la v7 et du traducteur dans meta...
herbelin
2005-12-20
*
correction d'un bug dans le make install
narboux
2005-12-15
*
Changement des named_context
gregoire
2005-12-02
*
commited new ring
barras
2005-11-18
*
Adds tools to help in defining new general recursive functions
bertot
2005-11-07
*
option -w y finalement pas admise par ocamlc <= 3.08.2
herbelin
2005-11-05
*
Compatibilité ocaml 3.09
herbelin
2005-11-04
*
new congruence
corbinea
2005-08-17
*
Subtac: traitement correct des existentielles et de la récursion.
coq
2005-07-15
*
reflexive tauto
corbinea
2005-07-15
*
dp: ajout des prédicats de sortes
coq
2005-06-24
*
dp: traitement des fixpoints
coq
2005-06-09
*
Forgot to remove a cmo.
coq
2005-05-25
*
Added subtac contrib.
coq
2005-05-25
*
dp: ajout du prouveur Zenon
coq
2005-05-24
*
Interface vers outil de recherche Whelp
herbelin
2005-05-20
*
Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...
herbelin
2005-05-17
*
appel de Simplify depuis Coq
coq
2005-03-18
*
tactiques prouveurs premier ordre dans contrib/dp/
coq
2005-03-16
*
Ajout de COQLIB/user-contrib à l'installation pour insister sur la possibili...
herbelin
2005-03-11
*
clean de parser.opt
herbelin
2005-03-01
*
Moving centralised discharge into dispatched discharge_function; required to ...
herbelin
2005-02-18
*
Ajout g_xml.ml4 et cic2Xml.ml
herbelin
2005-02-04
*
Nouveau fichier Tactics.v collectant les tactiques utiles des utilisateurs
herbelin
2005-02-03
*
Application du patch ebuild coq-8.0-r1 de la gentoo (uniformisation du Makefile)
herbelin
2005-02-01
*
Ajout dependance LIBCOQRUN pour coqide et coq-interface
herbelin
2005-01-25
*
Modification cible doc/coq.tex pour tenir des .mli qui n'existent pas toujour...
herbelin
2005-01-21
*
HUGE COMMIT
sacerdot
2005-01-03
*
Pour permettre le chargement des printers en ocamldebug >= 3.07 : renommage s...
herbelin
2005-01-02
*
Remplacement du coeur d'omega (omega.ml) par la version plus générale utili...
herbelin
2004-12-27
*
Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...
herbelin
2004-12-25
*
Names.substitution (and related functions) and Term.subst_mps moved to
sacerdot
2004-11-16
*
bug coqmktop avec libcoqrun.a en bytecode
barras
2004-11-15
*
autorewrite moved from HIGHTACTICS to TACTICS (to implement Printing
sacerdot
2004-11-05
*
COMMITED BYTECODE COMPILER
barras
2004-10-20
*
Tacred après Typing
herbelin
2004-10-18
*
no-assert en mode natif
herbelin
2004-09-26
*
error if binder was already defined
barras
2004-09-23
*
link order again
barras
2004-09-22
*
pbs with link order and deps
barras
2004-09-20
*
restructuration des printers: proofs passe avant parsing
barras
2004-09-17
*
repaired deps
barras
2004-09-17
*
hiding the meta_map in evar_defs
barras
2004-09-15
*
deplacement de clenv vers pretyping
barras
2004-09-03
*
premiere reorganisation de l\'unification
barras
2004-09-03
*
Dépendance en pa_ifdef dans la ligne camlp4deps de q_coqast induit make depe...
herbelin
2004-08-26
*
Utilisation de la variable camlp4 OCAML_308 plutôt que d'en reconstruire un...
herbelin
2004-07-27
*
Minimisation de l'utilisation de pa_ifdef.cmo pour éviter les messages d'obs...
herbelin
2004-07-20
*
Indépendance de parser vis a vis de ocamlrun
herbelin
2004-07-19
*
Bugs make clean
herbelin
2004-07-18
[next]