coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	Création du fichier dumpglob.ml, qui rassemble les fonctions de ↵	notin	2008-06-25
\| \| \| \| \| \|	globalisation (add_glob* et dump_*) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11177 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression de l'option -dump-glob et ajout d'une option -no-glob	notin	2008-06-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11167 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Documentation de admit et Print Assumptions.	herbelin	2008-06-09
\| \| \| \| \| \| \| \| \| \| \| \|	- Relecture, mise à jour, correction d'erreurs et petite réorganisation du chapitre sur les commandes vernaculaires. - Correction bug #1865 (rafraichissement des univers algébriques). - Suppression de la dépendance du initial.coq en les noms longs des fichiers de façons à ce que les dépendances ne soient que purement logique. - Encore un (petit) bug undo ide. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11077 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Correction d'un nouveau bug de undo de CoqIDE ("Admitted" et "Proof t"	herbelin	2008-05-30
\| \| \| \| \| \| \| \| \| \|	n'étaient pas gérés, merci à Julien). - Correction pb blocage CoqIDE quand le browser n'est pas déja lancé (utilisation pour cela de Sys.command au lieu de Unix.open_process_full). - MAJ CHANGES et COMPATIBILITY. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11022 85f007b7-540e-0410-9357-904b9bb8a0f7
*	debug : case where length of s is < 2...	jnarboux	2008-05-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11005 85f007b7-540e-0410-9357-904b9bb8a0f7
*	debug subst_command_placeholder : replace %s and not only %	jnarboux	2008-05-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10991 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used to	msozeau	2008-05-12
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	change the default pretty-printing to use Π, λ instead of forall and fun (and allow "," as well as "=>" for "fun" to be more consistent with the standard forall and exists syntax). Parsing allows theses new forms too, even if not in -unicode, and does not make Π or λ keywords. As usual, criticism and suggestions are welcome :) Not sure what to do about "->"/"→" ? - [setoid_replace by] now uses tactic3() to get the right parsing level for tactics. - Type class [Instance] names are now mandatory. - Document [rewrite at/by] and fix parsing of occs to support their combination. - Backtrack on [Enriching] modifier, now used exclusively in the implementation of implicit arguments. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10921 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suite 10904 (fichiers oubliés)	herbelin	2008-05-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10905 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient	herbelin	2008-04-01
\| \| \| \| \| \| \| \|	pas correctes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10739 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Plus de combinateurs sont passés de Util à Option. Le module Options	aspiwack	2007-12-06
	devient Flags. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10348 85f007b7-540e-0410-9357-904b9bb8a0f7