coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Suppression des stamps et donc des *_constraints	clrenard	2001-11-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2186 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suite de la suppression : enamed_declaration est remplace par evar_map.	clrenard	2001-11-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2164 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression des local_constraints, des ctxtty et du focus.	clrenard	2001-11-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2163 85f007b7-540e-0410-9357-904b9bb8a0f7
*	entetes	filliatr	2001-03-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout set_lc	herbelin	2000-12-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1162 85f007b7-540e-0410-9357-904b9bb8a0f7
*	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr	2000-12-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1090 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Traitement du pretty-print des Redexp	delahaye	2000-11-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@911 85f007b7-540e-0410-9357-904b9bb8a0f7
*	correction Abstract (et make world passe!)	filliatr	2000-11-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@794 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Renommage canonique :	herbelin	2000-10-18
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	declaration = definition \| assumption mode de reference = named \| rel Ex: push_named_decl : named_declaration -> env -> env lookup_named : identifier -> safe_environment -> constr option * typed_type add_named_assum : identifier * typed_type -> named_context -> named_context add_named_def : identifierconstrtyped_type -> named_context -> named_context git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@723 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
*	documentation	filliatr	2000-01-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@288 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
*	module Pfedit	filliatr	1999-12-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@169 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
*	- 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
*	modules Evar_refiner et Typing_ev	filliatr	1999-10-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@110 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 Proof_trees	filliatr	1999-10-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@104 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
*	deplacement des var. ex. dans proofs	filliatr	1999-10-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@94 85f007b7-540e-0410-9357-904b9bb8a0f7
*	quelques trucs necessaires au toplevel	filliatr	1999-09-28
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@84 85f007b7-540e-0410-9357-904b9bb8a0f7