coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Bugs	herbelin	2000-06-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@503 85f007b7-540e-0410-9357-904b9bb8a0f7
*	bugs infrence des arguments manquants dans le prdicat	herbelin	2000-06-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@494 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bugs et simplifications coercions	herbelin	2000-06-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@487 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	herbelin	2000-05-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@482 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
*	Effets de bords suite à la restructuration des inductives (cf Inductive)	herbelin	2000-05-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@442 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Renommage try_mutind_of en find_inductive (on fait ce qu'on peut !)	herbelin	2000-05-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@416 85f007b7-540e-0410-9357-904b9bb8a0f7
*	pattern-matching non-exhaustif (occur_rawconstr)	filliatr	2000-05-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@398 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Retrait fullmind de inductive_summary pour simplicité	herbelin	2000-04-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@376 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Introduction d'un type constr_pattern pour les différents filtrages	herbelin	2000-04-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@368 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extension du case_info : ajout du nombre de vrais args de chaque constr pour ↵	herbelin	2000-03-21
\| \| \| \| \| \|	la iota-réduction et d'autres informations pour l'affichage dans l'argument du cases git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@332 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Qqes bugs (evars dans le predicat; tag des cas défauts)	herbelin	2000-03-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@315 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Reparation bug isevars dans pretyping	herbelin	2000-03-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@309 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Un nouveau moteur pour Cases (phase 1)	herbelin	2000-03-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@302 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Abstraction de l'implémentation des signatures de Sign en vue intégration ↵	herbelin	2000-01-26
\| \| \| \| \| \|	du let-in git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@281 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction pbs liés aux evar	herbelin	2000-01-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@265 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug lift	herbelin	1999-12-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@258 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
*	Poursuite intégration du Cases	herbelin	1999-12-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@242 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Intégration initiale du Cases	herbelin	1999-12-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@234 85f007b7-540e-0410-9357-904b9bb8a0f7
*	modifs pour premiere edition de liens	filliatr	1999-12-02
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@189 85f007b7-540e-0410-9357-904b9bb8a0f7