coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Pourquoi normaliser le prédicat du Cases dans le noyau ? (casse la	herbelin	2002-12-10
\| \| \| \| \| \| \|	possibilité de partage) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3416 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Déplacement du hash-consing vers declare.ml	herbelin	2002-12-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3412 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Renoncement	herbelin	2002-08-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2962 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modules dans COQ\!\!\!\!	coq	2002-08-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵	herbelin	2002-05-29
\| \| \| \| \| \|	commandes vernaculaires (cf dev/changements.txt pour plus de précisions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2722 85f007b7-540e-0410-9357-904b9bb8a0f7
*	petite erreur dans le typage des let-in	barras	2002-03-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2573 85f007b7-540e-0410-9357-904b9bb8a0f7
*	petit nettoyage de kernel/inductive	barras	2002-02-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2460 85f007b7-540e-0410-9357-904b9bb8a0f7
*	compat ocaml 3.03	filliatr	2001-12-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2291 85f007b7-540e-0410-9357-904b9bb8a0f7
*	types vs constr	herbelin	2001-11-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2210 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suites modifs du noyau. Univ devient purement fonctionnel.	barras	2001-11-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2183 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Rétablissement de la persistance des Cast; typage des LetIn sans recours à ↵	herbelin	2001-11-08
\| \| \| \| \| \|	Cast git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2171 85f007b7-540e-0410-9357-904b9bb8a0f7
*	GROS COMMIT:	barras	2001-11-05
\| \| \| \| \| \| \| \| \| \|	- reduction du noyau (variables existentielles, fonctions auxiliaires pour inventer des noms, etc. deplacees hors de kernel/) - changement de noms de constructeurs des constr (suppression de "Is" et "Mut") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2158 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression des arguments sur les constantes, inductifs et constructeurs	barras	2001-10-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2106 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bugs de vérification de la bonne fondation en présence de définitions ↵	herbelin	2001-10-03
\| \| \| \| \| \|	locales dans le type de l'inductif décroissant git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2099 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles ↵	herbelin	2001-09-19
\| \| \| \| \| \|	des sortes (InProp, InSet, InType) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2009 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ↵	herbelin	2001-09-10
\| \| \| \| \| \|	éliminations, pour éviter les collisions avec les univers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1944 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ↵	herbelin	2001-07-21
\| \| \| \| \| \|	par le nombre d'args inutiles + vérification dans le noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1860 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Depliage des let-in dans le test de garde	herbelin	2001-07-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1822 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Normalisation du predicat synthetise pour les Case	clrenard	2001-06-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1798 85f007b7-540e-0410-9357-904b9bb8a0f7
*	erreur DeBruijn causant un RecursionNotOnInductiveType quand le type est un Let	letouzey	2001-05-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1763 85f007b7-540e-0410-9357-904b9bb8a0f7
*	amelioration des messages d'erreurs vis a vis des evars	barras	2001-05-23
\| \| \| \| \| \| \|	ajout automatique des chemins vers les sources au moment du Drop git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1761 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Changement de la structure des points fixes	barras	2001-05-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1731 85f007b7-540e-0410-9357-904b9bb8a0f7
*	amelioration de la structure des univers	barras	2001-03-28
\| \| \| \| \| \| \| \|	elimination des compteurs globaux de metas et d'evars du noyau nettoyage de safe_typing.ml (plus de flags) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1497 85f007b7-540e-0410-9357-904b9bb8a0f7
*	entetes	filliatr	2001-03-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Amélioration message d'erreur conditions de garde	herbelin	2001-03-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1455 85f007b7-540e-0410-9357-904b9bb8a0f7
*	nouvelle implantation de la reduction	barras	2001-03-01
\| \| \| \| \| \| \|	suppression de IsXtra du noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1416 85f007b7-540e-0410-9357-904b9bb8a0f7
*	retire profile	mohring	2001-02-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1413 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Changement de subst_meta	mohring	2001-02-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1412 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise en place d'un système optionnel de discharge immédiat; prise en ↵	herbelin	2001-02-14
\| \| \| \| \| \|	compte des défs locales dans les arguments des inductifs; nettoyage divers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1381 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Chgt signature de type_of_existential	herbelin	2001-02-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1341 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ commentaires	herbelin	2000-12-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1101 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Reparation conditions de positivites inductifs, echange dans add_entry	mohring	2000-12-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1057 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Déplacement du message d'erreur de gen_rel vers l'appelant pour le prétypage	herbelin	2000-11-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1011 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug dans la gestion du contexte en présence de Fix dans le calcul de garde	herbelin	2000-11-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@978 85f007b7-540e-0410-9357-904b9bb8a0f7
*	suppression des (* open Generic *)	filliatr	2000-11-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@793 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Simplifications autour de typed_type (renommé types par analogie avec ↵	herbelin	2000-10-18
\| \| \| \| \| \|	sorts); documentation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@727 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Renommage canonique :	herbelin	2000-10-18
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	declaration = definition \| assumption mode de reference = named \| rel Ex: push_named_decl : named_declaration -> env -> env lookup_named : identifier -> safe_environment -> constr option * typed_type add_named_assum : identifier * typed_type -> named_context -> named_context add_named_def : identifierconstrtyped_type -> named_context -> named_context git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@723 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Prise en compte de l'environnement dans les tests de bonne fondaison	herbelin	2000-10-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@691 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Prise en compte de Let dans build_dependent_inductive	herbelin	2000-10-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@683 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction incompatibilites dans la fn des types des inductifs	herbelin	2000-10-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@673 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Renommage AppL en App	herbelin	2000-10-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@634 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug message erreur	herbelin	2000-10-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@630 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Abstraction de constr	herbelin	2000-09-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@604 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modification mkAppL; abstraction via kind_of_term; changement dans Reduction	herbelin	2000-09-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@597 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction pour make doc	herbelin	2000-09-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@594 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression de Abst	herbelin	2000-09-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@593 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout d'un LetIn primitif.	herbelin	2000-09-10
\| \| \| \| \| \| \|	Abstraction de constr via kind_of_constr dans une bonne partie du code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@591 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Passage à des contextes de vars et de rels pouvant contenir des déclarations	herbelin	2000-07-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@568 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Plus de env et sigma dans get_arity, plus de sigma dans make_arity	herbelin	2000-07-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@549 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extension de find_inductive aux co-inductifs et renommage en find_rectype	herbelin	2000-07-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@542 85f007b7-540e-0410-9357-904b9bb8a0f7