coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	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
*	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 correction des inductifs	herbelin	2000-10-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@690 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
*	On laisse les LetIn dans les types des constructeurs et des éliminations	herbelin	2000-09-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@612 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
*	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
*	Précalcul de la forme canonique des constructeurs et arités pour traiter ↵	herbelin	2000-07-01
\| \| \| \| \| \|	les cas du fichier Ensemble.v sans avoir à renormaliser à chaque fois git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@548 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise en place d'un choix constr/typed_type en remplacement de certains Cast	herbelin	2000-06-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@484 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nettoyage de Generic;Suppression des DLAM en tête des listes de constructeurs	herbelin	2000-05-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@480 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suite restructuration inductifs; changement nom module Constant en Declarations	herbelin	2000-05-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@458 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajouts des causes d'erreur de Indrec	herbelin	2000-05-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@446 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Abstraction du type typed_type (un pas vers les jugements 2 niveaux)	herbelin	2000-04-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@362 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Prise en compte nouveau case_info	herbelin	2000-03-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@334 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nettoyage check_pos	herbelin	2000-03-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@294 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouveaux types 'constructor' et 'inductive' dans Term;	herbelin	1999-12-15
\| \| \| \| \| \| \| \| \|	les fonctions sur les inductifs prennent maintenant des 'inductive' en paramètres; elle n'ont plus besoin de faire des appels dangereux aux find_m*type qui centralisent la levée de raise Induc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@257 85f007b7-540e-0410-9357-904b9bb8a0f7
*	debuggage inductifs (suite) / compilation Dhyp et Auto (mais pas linkes	filliatr	1999-12-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@220 85f007b7-540e-0410-9357-904b9bb8a0f7
*	check_correct_par n'etait pas fait au bon endroit	filliatr	1999-12-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@213 85f007b7-540e-0410-9357-904b9bb8a0f7
*	explicitations erreurs inductifs	filliatr	1999-12-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@203 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Typing -> Safe_typing	filliatr	1999-12-01
\| \| \| \| \| \| \| \| \|	- proofs/Typing_ev -> pretyping/Typing - env -> sign - fonctions var_context git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@167 85f007b7-540e-0410-9357-904b9bb8a0f7
*	modules Indrec, Tacentries, Hiddentac	filliatr	1999-11-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@131 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- déplacement (encore une fois !) des variables existentielles : elles sont	filliatr	1999-10-18
\| \| \| \| \| \| \| \| \| \|	toujours dans le noyau (en ce sens que Reduction et Typeops les connaissent) mais dans un argument supplémentaire A COTE de l'environnement (de type unsafe_env) - Indtypes et Typing n'utilisent strictement que Evd.empty git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@106 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ensembles de contraintes d'univers	filliatr	1999-09-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@78 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ajout des inductifs (sans types singletons pour l'instant)	filliatr	1999-08-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@32 85f007b7-540e-0410-9357-904b9bb8a0f7
*	suppression champs inutiles dans constantes et inductifs; verification ↵	filliatr	1999-08-27
	definitions inductives git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@29 85f007b7-540e-0410-9357-904b9bb8a0f7