coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	amelioration mineur du comportement de Function	jforest	2008-11-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11625 85f007b7-540e-0410-9357-904b9bb8a0f7
*	first attempt to allow Function to deal with dependent pattern matching. ↵	jforest	2008-11-23
\| \| \| \| \| \|	This Functionnality is VERY VERY experimental and only works with non recursive functions and structurally defined function git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11624 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Synchronized subst_object with load_object (load_and_subst_objects)	herbelin	2008-11-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	and set Declare ML Module as a regular substitutive object so that Declare ML Module is treated at the right place in the order of appearance of substitutive declarations of a required module. - Note: The full load/import mechanism for modules is not so clear: the Require part of a Require Import inside a module is set outside the module at module closing but the Import part remains inside (why not to put the "special" objects in the module too?); moreover the "substitute" and "keep" objects of a module are desynchronised at module closing (is that really harmless/necessary?). - Treatment of .cmxs targets in coq_makefile and in coqdep. - Better make clean in coq_makefile generated makefiles. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11623 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fine-tuning rewriting from "eq_true b": using <- to rewrite true to b	herbelin	2008-11-23
\| \| \| \| \| \| \|	(if ever necessary). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11621 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Minor improvement to commit 11619	herbelin	2008-11-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11620 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed bug #2006 (type constraint on Record was not taken into account) +	herbelin	2008-11-23
\| \| \| \| \| \| \| \|	slight improving of the printing of record. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11619 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed bug in VernacExtend printing + missing vernacular printing rules +	herbelin	2008-11-22
\| \| \| \| \| \| \| \| \| \|	revival of option -translate as a -beautify option. PS: compilation checked against 11610. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11618 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Fixed minor bug #1994 in the tactic chapter of the manual [doc]	herbelin	2008-11-22
\| \| \| \| \| \| \| \| \| \| \| \| \|	- Improved warning when found several path to the same file in path [mltop.ml4, system.ml] - Add support for "rewrite" on specific equality to true (i.e. eq_true) [Datatypes.v, tactics] PS: compilation test made over 11611 to shunt the archive-breaking 11612 and 11614 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11617 85f007b7-540e-0410-9357-904b9bb8a0f7
*	fixed problem with r11612	barras	2008-11-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11614 85f007b7-540e-0410-9357-904b9bb8a0f7
*	fixed exponential behavior of evar unif (ground case)	barras	2008-11-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11612 85f007b7-540e-0410-9357-904b9bb8a0f7
*	correction of bug #2002	jforest	2008-11-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11610 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add implicit rules for native plugins (.cmxs)	glondu	2008-11-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11607 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Execute #rectypes directive in embedded OCaml toplevel...	glondu	2008-11-19
\| \| \| \| \| \| \|	...to avoid the need to have cflags.cmi around. This directive will likely be available in the next version of OCaml. See OCaml bug #4460. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11605 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix typo in omega doc	glondu	2008-11-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11604 85f007b7-540e-0410-9357-904b9bb8a0f7
*	integrate suggestions by B. Baydemir (see #1930)	letouzey	2008-11-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11600 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Univ: two < instead of a Pervasives.compare on int (as suggested by X. Leroy)	letouzey	2008-11-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11595 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correct display of constraints for Print Universes "dumpfile"	letouzey	2008-11-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11593 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Amélioration du README.doc et de l'installation de la doc	notin	2008-11-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11591 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Restores behaviour of v8.1 for unification problems which fail (backport of ↵	letouzey	2008-11-14
\| \| \| \| \| \|	11585) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11590 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Faster comparison of universes	letouzey	2008-11-14
\| \| \| \| \| \| \| \| \|	- compare the integer indexes first, in order to avoid comparing the dirpath part if possible - use an ad-hoc comparison function rather than Pervasives.compare (slightly faster during my tests on the compcert contrib) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11589 85f007b7-540e-0410-9357-904b9bb8a0f7
*	make doc ne compilait plus la doc de stdlib (bug #1996)	notin	2008-11-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11588 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add missing test-suite files for closed bugs.	msozeau	2008-11-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11587 85f007b7-540e-0410-9357-904b9bb8a0f7
*	retour sur le commit 11579 qui faisait plante les contribs FSet et color.	soubiran	2008-11-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11586 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Tentative d'amélioration de la robustesse des Makefile générés par	notin	2008-11-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	coq_makefile en présence de fichiers .ml : - ajout d'une option -config à coqtop qui affiche les informations de configuration (COQTOP, COQBIN, COQLIB, CAMLP4, CAMLP4LIB, CAMLBIN, LOCAL) - coq_makefile inclut un fichier Makefile.config qui contient les valeurs des variables sus-mentionnées git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11584 85f007b7-540e-0410-9357-904b9bb8a0f7
*	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11583 ↵	barras	2008-11-13
\| \| \| \|	85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction du bug #1995	notin	2008-11-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11580 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Les signatures des applications de foncteur sont précalculées, cela ↵	soubiran	2008-11-12
\| \| \| \| \| \| \| \| \|	alourdit un peu les vo mais accélère la compilation lorsque les foncteurs sont massivement utilisés. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11579 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Makefile.build: an OPTFLAGS behind a bytecode ocamlc (which refuses -p)	letouzey	2008-11-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11577 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix mixup between Record, Structure and Class by adding a new variant for	msozeau	2008-11-10
\| \| \| \| \| \| \|	the three cases. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11572 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix bug reported by Mark Dickinson on Coq-Club about [setoid_rewrite] not	msozeau	2008-11-10
\| \| \| \| \| \| \|	reducing the type of the given lemma. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11571 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Correction erreur dans test output Notation.v	herbelin	2008-11-09
\| \| \| \| \| \| \|	- Ajout test pour non-régression du bug #1968 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11569 85f007b7-540e-0410-9357-904b9bb8a0f7
*	f_equal : solve an inefficiency issue (apply vs. simple apply)	letouzey	2008-11-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11567 85f007b7-540e-0410-9357-904b9bb8a0f7
*	better fix for #1931 by using sort_of	letouzey	2008-11-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11566 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Oops... forgot to commit a file related to r11561.	msozeau	2008-11-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11565 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add test-suite file related to discussion of syntax of implicit binders.	msozeau	2008-11-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11564 85f007b7-540e-0410-9357-904b9bb8a0f7
*	More factorization of inductive/record and typeclasses: move class	msozeau	2008-11-09
\| \| \| \| \| \| \| \| \| \| \| \|	declaration code to toplevel/record, including support for singleton classes as definitions. Parsing code also factorized. Arnaud: one more thing to think about when refactoring the definitions in vernacentries. Add support for specifying what to do with anonymous variables in contexts during internalisation (fixes bug #1982), current choice is to generate a name for typeclass bindings. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11563 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Fixed bug 1968 (inversion failing due to a Not_found bug introduced in	herbelin	2008-11-09
\| \| \| \| \| \| \| \| \| \| \| \|	Evarutil.check_and_clear_in_constr in V8.2 revision 11309 and trunk revision 11300). - Improved various error messages related to inversion, evars and case analysis (including the removal of the obsolete dependent/non dependent distinction). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11561 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Apply vmconv if there are no _undefined_ evars around.	msozeau	2008-11-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11560 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Slight change of the semantics of user-given casts: they don't really	msozeau	2008-11-07
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	help the type _checking_ anymore (they don't become typing constraints) but they permit to coerce a subterm in a type. In particular, when using a VM cast we avoid unneeded, unexpected conversions using the default machine (oops!). Also remove the corresponding comment in pretyping and fix the wrong use of casts in toplevel/command: accept the trouble of using evars. This has the somewhat adverse effect that when typing casted object we now have no typing constraints (see e.g. examples in Cases.v)! Probably, this will be backtracked partially tomorrow as many contribs can rely on it and the change could make some unifications fail (in particular with deep coercions). Let's try anyway! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11558 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Ajout possibilité de lancer ocamldebug sur coqide	herbelin	2008-11-07
\| \| \| \| \| \| \| \| \|	- Correction bug #1815 sur "coqide dir_inexistant/nom_fichier" - Tests oubliés de la révision 11438 (amélioration affichage coercions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11555 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suite #11533	notin	2008-11-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11554 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction du bug #1926	notin	2008-11-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11553 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add some example uses of the new record features in Record.v:	msozeau	2008-11-07
\| \| \| \| \| \| \| \| \| \| \| \|	- introduction notation with missing fields and interaction with Program. - Ability to add (currently a single) "where notation" clause to each field. - Use every information available to do type inference and internalisation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11552 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix a bug in the specialization by unification tactic related to the problems	msozeau	2008-11-07
\| \| \| \| \| \| \| \|	given by injection. Add the example to the test-suite for [dependent destruction]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11551 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add the ability to give a specific tactic to solve each obligation in	msozeau	2008-11-07
\| \| \| \| \| \| \|	Program. No syntax to do it yet. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11550 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix universe problem appearing ConCaT using the existing infrastructure for	msozeau	2008-11-07
\| \| \| \| \| \| \| \| \| \|	declaring additional conversion problems when unifying the type of an evar instance and the evar's declared type. Fix the corresponding conversion heuristic which failed due to (misplaced?) assertions when faced with general conversion problems. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11549 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Cosmetic: no more whitespace at end of lines in extraction files	letouzey	2008-11-06
\| \| \| \| \| \|	(diff says it's a big commit, whereas diff -w says it's an empty one ;-) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11547 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction d'un petit bug en cas de redéfintion par l'utilisateur de ↵	notin	2008-11-06
\| \| \| \| \| \|	variables utilisées dans PP git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11546 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Minor fixes:	msozeau	2008-11-05
\| \| \| \| \| \| \| \| \|	- Rework definition of the type of respecful functions in Morphisms.v - Unfold [flip] in "Add Morphism" tactic (suggested by N. Tabareau) - Add a "coqvariableref" command in coqdoc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11545 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Port [rewrite] tactics to open terms. Currently no check that evars	msozeau	2008-11-05
\| \| \| \| \| \| \| \|	introduced by the lemma remain in the subgoals (i.e. it's really [erewrite]). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11544 85f007b7-540e-0410-9357-904b9bb8a0f7