coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	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
*	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
*	Centralisation prod_name and co dans Environ; mkLambda_string dans Term	herbelin	2000-05-18
\| \| \| \| \| \| \|	Effets de bords suite à la restructuration des inductives (cf Inductive) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@441 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout du langage de tactiques	delahaye	2000-05-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@401 85f007b7-540e-0410-9357-904b9bb8a0f7
*	erreurs lexicales dans les patterns (manquait des espaces)	filliatr	2000-03-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@359 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout {prod,lambda}_name	herbelin	2000-03-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@349 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Tauto	filliatr	2000-03-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@331 85f007b7-540e-0410-9357-904b9bb8a0f7
*	mauvais parenthesage dans hd_name (patterns imbriques)	filliatr	2000-03-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@317 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Utilisation de l'env pour nommer les Rel	herbelin	2000-03-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@316 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
*	gros commit de tout ce que j'ai fait pendant les vacances :	filliatr	2000-01-21
\| \| \| \| \| \| \| \| \| \|	- tactics/Equality - debug du discharge - constr_of_compattern implante vite fait / mal fait en attendant mieux - theories/Logic (ne passe pas entierrement) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@280 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
*	modules profile, Coqinit et Coqtop (=main)	filliatr	1999-12-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@194 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- environment -> safe_environment	filliatr	1999-12-01
\| \| \| \| \| \| \|	- unsafe_env -> env git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@168 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
*	Evd vient apres Environ -> id_of_existential expanse	filliatr	1999-11-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@147 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ajouts divers pour module Printer	filliatr	1999-11-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@145 85f007b7-540e-0410-9357-904b9bb8a0f7
*	typage des existentielles dans Typing_ev; suppression metamap inutiles dans ↵	filliatr	1999-11-25
\| \| \| \| \| \|	typage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@141 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Auto,Dhyp,Elim / Reduction de Evar / declarations eliminations	filliatr	1999-11-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@132 85f007b7-540e-0410-9357-904b9bb8a0f7
*	les variables existentielles contiennent maintenant un environnement (type	filliatr	1999-10-19
\| \| \| \| \| \| \| \|	unsafe_env) et non pas seulement une signature. Le module Evd vient donc apres le module Environ. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@108 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
*	module Logic	filliatr	1999-10-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@105 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- re-introduction d'une evar_map dans unsafe_env	filliatr	1999-10-13
\| \| \| \| \| \| \|	- les var. ex. sont des entiers, et non plus des section_path git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@99 85f007b7-540e-0410-9357-904b9bb8a0f7
*	deplacements des var. ex. hors du noyau	filliatr	1999-10-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@93 85f007b7-540e-0410-9357-904b9bb8a0f7
*	message erreur UI pendant import	filliatr	1999-09-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@79 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
*	- deplacement time stamps dans System (car utilise Unix)	filliatr	1999-09-08
\| \| \| \| \| \| \|	- dependances fichiers camlp4 (quelle merde !) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@56 85f007b7-540e-0410-9357-904b9bb8a0f7
*	mise en place repertoire test-suite/, toplevel/, parsing/	filliatr	1999-09-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@39 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- environnements vides	filliatr	1999-09-03
\| \| \| \| \| \| \| \|	- suppression du constructeur Implicit (et IsImplicit du coup) - nettoyages divers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@35 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
*	environnement sur	filliatr	1999-08-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@28 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- abstraction	filliatr	1999-08-26
\| \| \| \| \| \| \| \| \|	- univers fonctionnels - erreurs de typage maintenant sous forme d'exception, déclarées dans Type_errors git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@24 85f007b7-540e-0410-9357-904b9bb8a0f7
*	modules Instantiate, Constant et Inductive	filliatr	1999-08-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@22 85f007b7-540e-0410-9357-904b9bb8a0f7
*	mach et himsg; typage sans extraction	filliatr	1999-08-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@21 85f007b7-540e-0410-9357-904b9bb8a0f7
*	machine: execute = typage avec univers	filliatr	1999-08-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@18 85f007b7-540e-0410-9357-904b9bb8a0f7
*	module Reduction (fin)	filliatr	1999-08-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14 85f007b7-540e-0410-9357-904b9bb8a0f7
*	module Reduction (debut)	filliatr	1999-08-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12 85f007b7-540e-0410-9357-904b9bb8a0f7
*	module Closure	filliatr	1999-08-17
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11 85f007b7-540e-0410-9357-904b9bb8a0f7