index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
Commit message (
Expand
)
Author
Age
*
Utilisation de global_reference dans rawconstr
herbelin
2000-11-20
*
Utilisation de global_reference dans rawconstr
herbelin
2000-11-20
*
Utilisation de global_reference dans rawconstr; blindage pour quand appelé d...
herbelin
2000-11-20
*
Ajout erreur GlobalNotFound
herbelin
2000-11-20
*
Cablage des syntactif defs avec la Nametab des objets
herbelin
2000-11-20
*
Tables des eval_constant devient une Cstmap
herbelin
2000-11-20
*
methode export
filliatr
2000-11-15
*
Bugs lies a la confusion load/open et a un open abusivement recursif dans lib...
herbelin
2000-11-10
*
merge_loc
herbelin
2000-11-08
*
Insertion de coercion au milieu des applications partielles et propagation de...
herbelin
2000-11-08
*
Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de ...
herbelin
2000-11-06
*
nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...
filliatr
2000-11-06
*
correction Abstract (et make world passe!)
filliatr
2000-11-02
*
suppression des (* open Generic *)
filliatr
2000-11-02
*
Bug Simpl avec Cases cache sous plusieurs constantes
herbelin
2000-10-26
*
Petit nettoyage de Evarutil et Evarconv
herbelin
2000-10-23
*
Bug indices dans l'instance d'une evar
herbelin
2000-10-21
*
Nettoyage Coercion
herbelin
2000-10-19
*
Simplifications autour de typed_type (renommé types par analogie avec sorts)...
herbelin
2000-10-18
*
Renommage canonique :
herbelin
2000-10-18
*
Suppression d'un test inutile dans RCast
herbelin
2000-10-13
*
Renommage des find_m*type
herbelin
2000-10-11
*
Prise en compte de Let dans build_dependent_inductive
herbelin
2000-10-11
*
Bug affichage du nom des letin
herbelin
2000-10-11
*
Correction de bugs (alias initiaux et ordre des cas par défaut)
herbelin
2000-10-10
*
Messages d'erreurs Cases
herbelin
2000-10-10
*
Correction incompatibilites dans la fn des types des inductifs
herbelin
2000-10-06
*
Bugs de la réduction de Fix dans Simpl
herbelin
2000-10-05
*
Nouvelle stratégie de nommage dans Simpl pour Fix
herbelin
2000-10-04
*
Nouveau bug dans la réduction de Fix par red_elim_const
herbelin
2000-10-04
*
Renommage AppL en App
herbelin
2000-10-01
*
Renommage AppL en App; Suppression cast
herbelin
2000-10-01
*
Plus de whd_castapp
herbelin
2000-10-01
*
renommage map_constr_with_named_binders
herbelin
2000-10-01
*
Disparition du type oper mais nouveau type global_reference
herbelin
2000-10-01
*
Déplacement 'a reference et binder_kind de Term vers Rawterm
herbelin
2000-10-01
*
Nettoyage pretyping; ise_resolve_* devient understand_*; Ajout d'une notion d...
herbelin
2000-09-26
*
Minor correction for Ocamlweb + doc update
coq
2000-09-14
*
Abstraction de constr
herbelin
2000-09-14
*
Déplacement de fonctions de Reduction vers Tacred
herbelin
2000-09-14
*
Modification mkAppL; abstraction via kind_of_term; changement dans Reduction
herbelin
2000-09-12
*
Vers la paramétrisation des fonctions de Reduction et vers la fusion de
herbelin
2000-09-12
*
Correction pour make doc
herbelin
2000-09-10
*
Suppression de Abst
herbelin
2000-09-10
*
Ajout d'un LetIn primitif.
herbelin
2000-09-10
*
Canonisation de certains noms dans Pretyping, Asterm et Safe_typing
herbelin
2000-09-06
*
kernel/type_errors.ml
herbelin
2000-09-06
*
reparation bug des coercions (cas ou on importe une coercion faisant
barras
2000-08-08
*
Passage à des contextes de vars et de rels pouvant contenir des déclarations
herbelin
2000-07-24
*
Modifs d'interpretation de patterns
delahaye
2000-07-21
[next]