index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
Commit message (
Expand
)
Author
Age
*
Ajout d'une fonction de remplacement d'un sous-terme par un terme.
clrenard
2001-05-15
*
nettoyage extraction
filliatr
2001-05-09
*
Changement de la structure des points fixes
barras
2001-05-03
*
interdiction occ positives ET negatives dans Pattern
werner
2001-04-24
*
reduction des let in dans whd_programs
filliatr
2001-04-23
*
un typage sûr pour Goal et Check
filliatr
2001-04-20
*
to_constr renvoie directement un constr pour contourner l'ancien Term.mk_cons...
herbelin
2001-04-15
*
Suppression de mk_constr qui ne respectait pas l'invariant des applications (...
herbelin
2001-04-15
*
réparation d'un bug de Correctness: whd_programs ne doit pas réduire les te...
filliatr
2001-04-11
*
réparation Correctness; options Extraction (changement de syntaxe)
filliatr
2001-04-10
*
mise a jour pour ocamlweb
filliatr
2001-04-02
*
amelioration de la structure des univers
barras
2001-03-28
*
amelioration de la consommation memoire de la conversion en eta-expansant
barras
2001-03-23
*
entetes
filliatr
2001-03-15
*
Prise en compte des Let dans l'instance des evars
herbelin
2001-03-14
*
Amélioration message d'erreur conditions de garde
herbelin
2001-03-12
*
Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisation
herbelin
2001-03-11
*
corrections de bug de la reduction
barras
2001-03-08
*
compare_constr independent du groupement des applications.
barras
2001-03-08
*
réparation (?) discharge axiome
filliatr
2001-03-06
*
Re-Déplacement extended_rel_list
herbelin
2001-03-05
*
Déplacement de qualid dans Nametab, hors du noyau
herbelin
2001-03-01
*
nouvelle implantation de la reduction
barras
2001-03-01
*
retire profile
mohring
2001-02-28
*
Changement de subst_meta
mohring
2001-02-28
*
ident au lieu de string pour le nom de base de qualid
herbelin
2001-02-16
*
Mise en place d'un système optionnel de discharge immédiat; prise en compte...
herbelin
2001-02-14
*
simplification du make depend; fonctions de stat. util. memoire dans certains...
filliatr
2001-02-08
*
Chgt signature de type_of_existential
herbelin
2001-02-07
*
Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref
herbelin
2001-02-07
*
Mise en place de la possibilite d'unfolder des variables locales et des const...
filliatr
2001-01-31
*
Ajout d'espace dans les règles d'affichage des infix si des lettres figurent...
herbelin
2001-01-31
*
make doc
herbelin
2001-01-27
*
Ajout alias mutual_inductive_path = section_path
herbelin
2001-01-27
*
Ajout global_vars_decl
herbelin
2001-01-24
*
Doc
herbelin
2001-01-24
*
Déplacement du type stack de Reduction vers Closure et utilisation pour accÃ...
herbelin
2000-12-26
*
Alias variable_path
herbelin
2000-12-25
*
Bug mauvais environnement dans le test d'eta-conversion
herbelin
2000-12-20
*
Export de it_mkProd_or_LetIn_name et it_mkLambda_or_LetIn_name
herbelin
2000-12-18
*
Le bon choix, c'est finalement identifier = string
herbelin
2000-12-15
*
Mise en place d'un module Ident avec test de l'efficacité quand identifier=s...
herbelin
2000-12-15
*
- suppression mind_extract_params
filliatr
2000-12-15
*
Petite réorganisation
herbelin
2000-12-15
*
Les params d'inductif deviennent en même temps propre à chaque inductif d'u...
herbelin
2000-12-14
*
Les params d'inductif deviennent en même temps propre à chaque inductif d'u...
herbelin
2000-12-14
*
MAJ commentaires
herbelin
2000-12-14
*
Raffinement erreur Wrong Predicate
herbelin
2000-12-14
*
syntaxe AST Inversion + commentaires ocamlweb autour de $
filliatr
2000-12-12
*
Reparation conditions de positivites inductifs, echange dans add_entry
mohring
2000-12-06
[next]