coq - The formal proof system

Age	Commit message (Collapse)	Author
1999-10-19	module Refiner	filliatr
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@109 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	mise en place module Refiner	filliatr
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@107 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-14	module Proof_trees	filliatr
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@104 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-10-13	- re-introduction d'une evar_map dans unsafe_env	filliatr
	- 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
1999-10-13	redeplacement des var. ex. dans kernel :-)	filliatr
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@97 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
1999-10-08	deplacement des var. ex. dans proofs	filliatr
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@94 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-09-28	quelques trucs necessaires au toplevel	filliatr
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@84 85f007b7-540e-0410-9357-904b9bb8a0f7