index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
retyping.ml
Commit message (
Expand
)
Author
Age
...
*
Correction du bug des types singletons pas sous-type de Set
herbelin
2008-04-27
*
Application de refresh_universes dans typing.ml et retyping.ml : les
herbelin
2008-03-15
*
Compatibilité du polymorphisme de constantes avec les sections.
herbelin
2006-10-29
*
Extension du polymorphisme de sorte au cas des définitions dans Type.
herbelin
2006-10-28
*
- Indtypes: en attente opinion CoRN, les occurrences de Type non explicites
herbelin
2006-05-28
*
Nouvelle implantation du polymorphisme de sorte pour les familles inductives
herbelin
2006-05-23
*
Inductifs avec polymorphisme de sorte (version initiale)
herbelin
2006-03-29
*
Changement des named_context
gregoire
2005-12-02
*
Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changed
sacerdot
2005-01-14
*
premiere reorganisation de l\'unification
barras
2004-09-03
*
Nouvelle en-tête
herbelin
2004-07-16
*
Set is not always impredicative
barras
2004-01-12
*
Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern
herbelin
2003-05-19
*
Intégration des modifs de la branche mowgli :
herbelin
2002-11-05
*
Renoncement à distinguer les types "constr" et "types"; nettoyage
herbelin
2002-08-13
*
un cas inutile dans un pattern matching
letouzey
2002-07-16
*
petit nettoyage de kernel/inductive
barras
2002-02-07
*
exceptionmal ratrappee
barras
2002-02-04
*
Grossière erreur de typage
herbelin
2001-12-18
*
Suites modifs du noyau. Univ devient purement fonctionnel.
barras
2001-11-12
*
GROS COMMIT:
barras
2001-11-05
*
Blindage, de peur que des types entrant non en forme normale ne provoque des ...
herbelin
2001-09-19
*
Nouvelle fonction sort_family_of pour calculer la famille dans lequel vit un ...
herbelin
2001-09-19
*
Passage aux univers algébriques
herbelin
2001-09-09
*
Changement de la structure des points fixes
barras
2001-05-03
*
entetes
filliatr
2001-03-15
*
nouvelle implantation de la reduction
barras
2001-03-01
*
Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref
herbelin
2001-02-07
*
Bug env vis à vis du let in
herbelin
2000-12-15
*
suppression des (* open Generic *)
filliatr
2000-11-02
*
Simplifications autour de typed_type (renommé types par analogie avec sorts)...
herbelin
2000-10-18
*
Renommage canonique :
herbelin
2000-10-18
*
Renommage AppL en App
herbelin
2000-10-01
*
Modification mkAppL; abstraction via kind_of_term; changement dans Reduction
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
*
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
*
Plus de env et sigma dans get_arity, plus de sigma dans make_arity
herbelin
2000-07-01
*
Extension de find_inductive aux co-inductifs et renommage en find_rectype
herbelin
2000-07-01
*
Achèvement abstraction du mécanisme (optionnel) de cast
herbelin
2000-06-29
*
Mise en place d'un choix constr/typed_type en remplacement de certains Cast
herbelin
2000-06-01
*
Nettoyage de Generic
herbelin
2000-05-31
*
Effets de bords suite à la restructuration des inductives (cf Inductive)
herbelin
2000-05-18
*
Réorganisation
herbelin
2000-05-05
*
Renommage try_mutind_of en find_inductive (on fait ce qu'on peut !)
herbelin
2000-05-04
*
Ajout du langage de tactiques
delahaye
2000-05-03
*
Extension du case_info : ajout du nombre de vrais args de chaque constr pour ...
herbelin
2000-03-21
*
MAJ nouveau try_mutind_of
herbelin
2000-03-08
[prev]
[next]