coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	Nouveaux points d'accès pour les noms qualifiés	herbelin	2000-11-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@868 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Renommage canonique SectionLocalDecl -> SectionLocalAssum	herbelin	2000-11-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@837 85f007b7-540e-0410-9357-904b9bb8a0f7
*	out_variable (Liboject.obj -> ...) distibgue de get_variable	filliatr	2000-11-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@821 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de ↵	herbelin	2000-11-06
\| \| \| \| \| \|	DischargeAt) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@811 85f007b7-540e-0410-9357-904b9bb8a0f7
*	nouveau discharge fait par le noyau; plus de recettes dans les corps des ↵	filliatr	2000-11-06
\| \| \| \| \| \|	constantes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@807 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@724 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Disparition du type oper mais nouveau type global_reference	herbelin	2000-10-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@620 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Passage à des contextes de vars et de rels pouvant contenir des déclarations	herbelin	2000-07-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@568 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
*	portage Omega (code seulement)	filliatr	2000-04-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@381 85f007b7-540e-0410-9357-904b9bb8a0f7
*	discharge des axiomes	filliatr	2000-04-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@366 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
*	modules	filliatr	1999-12-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@238 85f007b7-540e-0410-9357-904b9bb8a0f7
*	deplacement de Discharge dans toplevel	filliatr	1999-12-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@222 85f007b7-540e-0410-9357-904b9bb8a0f7
*	declarations eliminations / debuggae inductifs (debut)	filliatr	1999-12-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@212 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- global_reference traite des variables	filliatr	1999-12-03
\| \| \| \| \| \| \| \| \|	- construct_reference, avec environnement en argument - link de Class - Definition et Check au toplevel git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@193 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
*	Pfedit (fin)	filliatr	1999-12-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@188 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
*	mise au point Declare et avancee dans Astterm	filliatr	1999-12-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@175 85f007b7-540e-0410-9357-904b9bb8a0f7
*	make_strength / reset_library	filliatr	1999-12-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@171 85f007b7-540e-0410-9357-904b9bb8a0f7
*	portage Astterm (partiellement)	filliatr	1999-11-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@159 85f007b7-540e-0410-9357-904b9bb8a0f7
*	module Classops; ajout de fonctions dans Declare en consequence	filliatr	1999-11-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@152 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
*	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
*	module Tactics (debut)	filliatr	1999-11-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@129 85f007b7-540e-0410-9357-904b9bb8a0f7
*	module Pattern, Wcclausenv (interface) et Tacticals	filliatr	1999-11-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@126 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- module Redinfo dans library/ pour les constantes d'élimination	filliatr	1999-10-22
\| \| \| \| \| \| \|	- module Tacred : fonctions de reductions utilisees dans les tactiques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@114 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
*	module Declare	filliatr	1999-09-19
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@77 85f007b7-540e-0410-9357-904b9bb8a0f7