coq - The formal proof system

Age	Commit message (Collapse)	Author
1999-11-19	module Pattern, Wcclausenv (interface) et Tacticals	filliatr
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@126 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-10-20	module Clenv (debut)	filliatr
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@111 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-10-20	modules Evar_refiner et Typing_ev	filliatr
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@110 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-10-19	les variables existentielles contiennent maintenant un environnement (type	filliatr
	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
1999-10-18	- déplacement (encore une fois !) des variables existentielles : elles sont	filliatr
	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
1999-10-14	module Logic	filliatr
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@105 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-10-08	module Logic (ne compile pas encore)	filliatr
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@95 85f007b7-540e-0410-9357-904b9bb8a0f7