coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	~keep_sections was now redundant. Got rid of.	sacerdot	2004-04-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5627 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fake dependent types in constructors of inductive types are now preserved.	sacerdot	2004-03-31
\| \| \| \| \| \| \| \| \| \| \|	The idea is: 1. constructors are always declare by hand by the user ==> binders always have a meaning. 2. the binders are fundamental for record fields, even if the dependent product is really non-dependent. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5621 85f007b7-540e-0410-9357-904b9bb8a0f7
*	syntax error: dandling in	sacerdot	2004-03-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5612 85f007b7-540e-0410-9357-904b9bb8a0f7
*	2 choix incorrects	herbelin	2004-03-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5610 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fabrication de l'uri a partir du path utilisateur	herbelin	2004-03-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5608 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix and Cofix blocks with mutually defined functions having the same	sacerdot	2004-03-25
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	name generated XML code with ambiguous names. Example: Inductive t : Set := k : t' -> t with t' : Set := k' : t -> t'. Scheme t_csc := Induction for t Sort Prop with t'_csc := Induction for t' Sort Prop. Print XML t_csc. used to show two functions both named F. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5568 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Comment removed.	sacerdot	2004-03-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5559 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ Claudio pour v8	herbelin	2004-03-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5552 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	barras	2003-03-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Petit netoyage dans lib	coq	2002-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3463 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t" - "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième pretty-printer dans ppconstr.ml est basé sur "constr_expr". - Nouveau répertoire "interp" qui hérite de la partie interprétation qui se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml; constrextern.ml est l'équivalent de termast.ml pour le nouveau printer; topconstr.ml; contient la définition de "constr_expr"; modintern.ml remplace astmod.ml) - Libnames.reference tend à remplacer Libnames.qualid git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Intégration de la branche mowgli	herbelin	2002-11-05
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3213 85f007b7-540e-0410-9357-904b9bb8a0f7