coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	Discharge (encore bugge)	filliatr	1999-12-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@223 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
*	correction bug construct_reference	filliatr	1999-12-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@219 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Intégration du Termast et du Retyping de HH, et modifications connexes	herbelin	1999-12-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@185 85f007b7-540e-0410-9357-904b9bb8a0f7
*	poursuite de Vernacentries	filliatr	1999-12-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@178 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
*	Backtrack sur modif Evd.evd_concl	herbelin	1999-11-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@139 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ pour fusion avec pretyping	herbelin	1999-11-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@138 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
*	- documentation repertoire proofs/	filliatr	1999-10-20
\| \| \| \| \| \| \| \|	- IsAppL of constr * constr list ==> répercussion - module Clenv (suite; as terminé) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@113 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
*	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
*	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
*	- minicoq : definition inductifs; syntaxe a->b	filliatr	1999-09-07
\| \| \| \| \| \| \| \|	- kernel : bug Typing/one_inductive (il fallait chercher l'arite typée dans l'environnement avec lookup_rel et non lookup_var) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@43 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
*	mach -> typing; machops -> typeops	filliatr	1999-08-26
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@27 85f007b7-540e-0410-9357-904b9bb8a0f7