coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	induction now admits multiple induction arguments. The principle must	coq	2006-02-10
\| \| \| \| \| \| \| \| \| \| \| \| \|	be explicitely given, and ALL parameters and args of the scheme must be given (only branches must be omitted). For the moment, only principle like generated by GenFixpoint (functional induction) are usable. That is the predicate must have a additional paramter like in: (P x1 ... xn (f p1...pm x1...xn)) Example of use : induction x y (add x y) using add_ind. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8023 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout option 'using lemmas' à auto/trivial/eauto	herbelin	2006-01-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7937 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout de la contrainte que l'assertion doit être complètement prouvée ↵	herbelin	2006-01-21
\| \| \| \| \| \|	dans 'assert by' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7910 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Retrait de 'by' comme mot-clé en espérant qu'il n'y aura pas ↵	herbelin	2006-01-18
\| \| \| \| \| \|	d'interférence avec des notations utilisateurs qui le remettrait mot-clé plus tard git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7888 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq	herbelin	2006-01-16
\| \| \| \| \| \| \| \|	choisir un nom; utilisation de IntroAnonymous au lieu de None dans l'argument "with_names" des tactiques induction, inversion et assert. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7880 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses	herbelin	2006-01-16
\| \| \| \| \| \| \| \|	- New tactic "pose proof" that generalizes "assert (id:=p)" with intro patterns - TacTrueCut and TacForward merged into new TacAssert bound to Tactics.forward git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7875 85f007b7-540e-0410-9357-904b9bb8a0f7
*	cvs ci -m "Passage à la limite dans les intro-pattern de n-uplets"	herbelin	2006-01-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7874 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression redondance coerce_to_id dans Pcoq et constrintern et ↵	herbelin	2006-01-09
\| \| \| \| \| \|	déplacement dans Topconstr git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7826 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Renommage des Ppnew en Pp (et déplacement dans parsing); renommage des ↵	herbelin	2005-12-26
\| \| \| \| \| \|	G_new en G_.ml + autres petites modifications liées à suppression du traducteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7740 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
*	Added 'clear - id' to clear all hypotheses except the ones dependent in the ↵	herbelin	2005-03-07
\| \| \| \| \| \|	statement of id git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6807 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added 'clear - id' to clear all hypotheses except the ones dependent in the ↵	herbelin	2005-03-07
\| \| \| \| \| \|	statement of id git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6806 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ExtraRedExpr maintenant sans argument: pas très souple mais au moins ↵	herbelin	2004-12-29
\| \| \| \| \| \|	convient pour l'exemple de MapleMode qui lui ne passait pas quand un argument était exigé git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6526 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Restauration type casted_open_constr pour tactique refine car l'unification ↵	herbelin	2004-12-09
\| \| \| \| \| \|	n'est pas assez puissante pour retarder la coercion vers le but au dernier moment git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6458 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Uniformisation du nom d'entrée openconstr en le nom du type open_constr	herbelin	2004-12-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6426 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des ↵	herbelin	2004-12-06
\| \| \| \| \| \|	tactiques d'appliquer une éventuelle coercion vers le but git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6408 85f007b7-540e-0410-9357-904b9bb8a0f7
*	COMMITED BYTECODE COMPILER	barras	2004-10-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression quotify	herbelin	2004-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5922 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouvelle en-tête	herbelin	2004-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
*	moved instantiate binding to extratactics	corbinea	2004-06-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5852 85f007b7-540e-0410-9357-904b9bb8a0f7
*	more evar stuff	corbinea	2004-06-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5843 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id ↵	herbelin	2004-03-02
\| \| \| \| \| \|	variable de ltac substituable dans la pratique par un intro_case_pattern dans induction, destruct et inversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5415 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Généralisation du type ltac Identifier en IntroPattern; prise en compte ↵	herbelin	2004-03-01
\| \| \| \| \| \|	des IntroPattern au parsing, à l'interprétation, à la traduction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5405 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout 'as (x,...,y)' dans NewDestruct et NewInd, NewInduction, ...	herbelin	2004-01-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5253 85f007b7-540e-0410-9357-904b9bb8a0f7
*	bugs avec Pose et Assert	barras	2004-01-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5190 85f007b7-540e-0410-9357-904b9bb8a0f7
*	meilleure presentation des commentaires du traducteur	barras	2004-01-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5168 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouvelle tactique EExists	clrenard	2003-12-01
\| \| \| \| \| \| \|	Changement des exports pour tactic EXTEND : with_bindings devient bindings qui prend plus le with, il faut le mettre à la main dans la règle. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5052 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Uniformisation des politiques de nommage de NewDestruct sur arguments ↵	herbelin	2003-11-25
\| \| \| \| \| \|	recursifs et Induction style Hrec; mise en place systeme de traduction automatique; Elim/Case reconnaissent les premisses nommees du but git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4989 85f007b7-540e-0410-9357-904b9bb8a0f7
*	New tactics : econstructor, eleft, eright, esplit	clrenard	2003-11-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4929 85f007b7-540e-0410-9357-904b9bb8a0f7
*	factorisation et generalisation des clauses	barras	2003-11-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4892 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Traduction semantique des InHyp de clause en InHypValue si local def	herbelin	2003-11-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4841 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added Instantiate ... in	corbinea	2003-11-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4820 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Cablage en dur de inversion	herbelin	2003-10-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4566 85f007b7-540e-0410-9357-904b9bb8a0f7
*	changement nouvelle syntaxe (pt fixes)	barras	2003-10-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4559 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et ↵	herbelin	2003-09-12
\| \| \| \| \| \| \| \| \|	choix du parseur en fonction de cette option git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4387 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout 'Symmetry in Hyp'	herbelin	2003-06-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4185 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Utilisation de intro_pattern dans NewDestruct/NewInduction	herbelin	2003-06-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4154 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression définitive de lmatch et or_metanum dans tacinterp	herbelin	2003-05-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4054 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin	2003-05-19
\| \| \| \| \| \| \| \| \|	Utilisation d'ident plutôt que int pour PMeta/CPatVar Ajout CEvar pour la saisie des Evar Pas d'entrée utilisateur pour les Meta noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4033 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin	2003-04-07
\| \| \| \| \| \| \| \| \|	pour compatibilité avec les modules. Globalisation partielle des invocations de tactiques hors définitions (partielle car noms des Intros/Assert/Inversion/... non connus). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3857 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug pattern_occ_hyp_list	herbelin	2003-03-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3818 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
*	Légère amélioration des messages d'erreur des with-bindings et des Rewrite	herbelin	2002-12-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3474 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout Simpl et Change sur des sous-termes	herbelin	2002-12-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3392 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
*	Ajout d'un suffixe "as [ names ]" pour nommer manuellement les	herbelin	2002-10-21
\| \| \| \| \| \| \|	variables introduites par NewDestruct et NewInduction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3169 85f007b7-540e-0410-9357-904b9bb8a0f7
*	NewDestruct/NewInduction acceptent l'option "using"	herbelin	2002-10-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3167 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Finalement un seul constr pour l'instant dans ExtraRedExpr	herbelin	2002-05-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2735 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵	herbelin	2002-05-29
\| \| \| \| \| \|	commandes vernaculaires (cf dev/changements.txt pour plus de précisions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2722 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout de l'entrée ne_constrarg_list	delahaye	2002-03-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2543 85f007b7-540e-0410-9357-904b9bb8a0f7