coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Utilisation du module Buffer; encodage plus rigoureux des symboles en uri	herbelin	2005-05-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7082 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction of a bug in functional scheme. It raised with mutual	coq	2005-05-26
\| \| \| \| \| \| \| \| \|	functions with imbricated recursive calls. Two bugs in one actually, one in the building of the set of recursive functions, and one with De Bruijn indices when looking for recursve calls. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7080 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Patch to avoid Whelp bug removed.	sacerdot	2005-05-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7079 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add a guard for V7 mode, CVS compiles cleanly again :)	coq	2005-05-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7078 85f007b7-540e-0410-9357-904b9bb8a0f7
*	New environment variable COQREMOTEBROWSER to set the command used by Coq	sacerdot	2005-05-26
\| \| \| \| \| \| \| \|	and coqide to control a remote browser. It uses the standard syntax where "%s" is the placeholder for the URL. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7077 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-05-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7075 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Forgot to remove a cmo.	coq	2005-05-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7074 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added subtac contrib.	coq	2005-05-25
\| \| \| \| \| \| \|	Added some debug printer in termops. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7073 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-05-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7071 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-05-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7070 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added clenv_environments_evars that behaves as clen_environments but	sacerdot	2005-05-24
\| \| \| \| \| \| \| \| \|	generating evars in place of metas. Notice that thanks to this changement unification can be more effective (expecially after reduction) since evars have non-empty contexts whereas metas have not. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7069 85f007b7-540e-0410-9357-904b9bb8a0f7
*	New commit to allow definitions of morphisms on relations whose carrier is	sacerdot	2005-05-24
\| \| \| \| \| \| \| \| \| \| \| \|	a Prod. Example: m : feq ==> feq where m has type (A -> B) -> (C -> D) and few is a relation over (fun X Y: Type. X -> Y). The problem is to avoid the interpretation (A -> B) -> C -> D that tries to use feq over D and feq over C considering (A -> B) as a quantification. This closes a wish of Bas Spitters. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7068 85f007b7-540e-0410-9357-904b9bb8a0f7
*	WARNING: unification changed (to fix a bug).	sacerdot	2005-05-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	1. When matching ?i[sigma] against t' in some cases ?i was instantiated with t' ignoring the explicit substitution sigma (i.e. always doing mimick); however, when t' occurs in sigma ?i can be instatiated with a Var/Rel (i.e. doing projection). The new behaviour is not equivalent to the old one (even up to bugs) since the new behaviour may accept not well typed instantiations and fail only later whereas the old (but buggy) behaviour failed immediately. 2. Second bug fixed: it was the case that instantiating and evar doing projection did not check whether the body of the evar contained metavariables (that breaks a Coq invariant). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7067 85f007b7-540e-0410-9357-904b9bb8a0f7
*	dp: ajout du prouveur Zenon	coq	2005-05-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7066 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-05-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7064 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Consequence of allowing the numerical argument of auto to be an ident for ltac	herbelin	2005-05-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7062 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug fix for a bug reported by Roland: the function that detects the constants	sacerdot	2005-05-23
\| \| \| \| \| \| \| \| \| \| \|	to be expanded during functor application was written supposing that the module had already been checked against its signature. However, this is actually a false hypothesis. The bug fix consists in replacing an "assert false" with the error message that would be obtained type checking the module against its module type. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7061 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-05-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7059 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-05-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7057 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-05-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7055 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-05-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7054 85f007b7-540e-0410-9357-904b9bb8a0f7
*	New command: "Print Ltac qualid" to print user defined tactics.	sacerdot	2005-05-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7053 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Adoption du nom canonique global_of_constr pour éviter confusion avec type ↵	herbelin	2005-05-20
\| \| \| \| \| \|	reference git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7052 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Déplacement et export de locate_global (ex-locate_reference) de tacinterp ↵	herbelin	2005-05-20
\| \| \| \| \| \|	vers syntax_def git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7051 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Déplacement et export de locate_global (ex-locate_reference) de tacinterp ↵	herbelin	2005-05-20
\| \| \| \| \| \|	vers syntax_def; Adoption du nom canonique global_of_constr pour éviter confusion avec type reference git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7050 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Interface vers outil de recherche Whelp	herbelin	2005-05-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7049 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Adoption du nom canonique global_of_constr pour éviter confusion avec type ↵	herbelin	2005-05-20
\| \| \| \| \| \|	reference git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7048 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation	herbelin	2005-05-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7047 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Achèvement du déplacement de fonctionnalités unix et browser de ide vers lib	herbelin	2005-05-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7046 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-05-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7044 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-05-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7043 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation	herbelin	2005-05-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7042 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Déplacement de fonctionnalités unix et browser de ide vers lib	herbelin	2005-05-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7041 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Setoid_replace: improved error message when trying to replace a term in a	sacerdot	2005-05-19
\| \| \| \| \| \| \|	non-applicative context. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7040 85f007b7-540e-0410-9357-904b9bb8a0f7
*	A wish by Bas Spitters granted: a little more of unification up to	sacerdot	2005-05-19
\| \| \| \| \| \| \| \|	convertibility is now tried in setoid_rewrite. As a consequence it is now possible to declare relations over the function space (fun A B: Type => A -> B). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7039 85f007b7-540e-0410-9357-904b9bb8a0f7
*	added VernacBacktrack (new backtracking command dedicated to	coq	2005-05-19
\| \| \| \| \| \| \| \|	interfaces like PG, coqied or pcoq) in order to get rid of a pattern matching not exhaustive. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7038 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-05-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7036 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-05-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7035 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Implemented autorewrite with ... in hyp [using ...].	sacerdot	2005-05-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7034 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-05-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7032 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-05-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7031 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Affinements suite à extension Tactic Notation aux tacticielles	herbelin	2005-05-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7030 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extension de Tactic Notation pour permettre d'tendre et de faire rffrence ↵	herbelin	2005-05-17
\| \| \| \| \| \|	aux niveaux syntaxiques des tacticielles git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7029 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extension de Tactic Notation pour permettre d'tendre et de faire rffrence ↵	herbelin	2005-05-17
\| \| \| \| \| \|	aux niveaux syntaxiques des tacticielles + erreur typage TacAlias git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7028 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-05-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7026 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-05-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7024 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-05-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7023 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Globalisation des Tactic Notation	herbelin	2005-05-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7022 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Allow auto to have a parametric argument (wish #967)	herbelin	2005-05-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7020 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Allow auto to have a parametric argument (wish #967)	herbelin	2005-05-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7019 85f007b7-540e-0410-9357-904b9bb8a0f7