coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Cleaning/uniformizing the interface of tacticals.mli	herbelin	2009-03-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11980 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Uniformisation du format des messages d'erreur (commencent par une	herbelin	2008-07-17
\| \| \| \| \| \| \| \| \| \|	majuscule - si pas un ident ou un terme - et se terminent par un point). Restent quelques utilisations de "error" qui sont liées à des usages internes, ne faudrait-il pas utiliser des exceptions plus spécifiques à la place ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11230 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Implantation de la suggestion 1873 sur discriminate. Au final,	herbelin	2008-06-21
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	discriminate/injection/simplify_eq acceptent maintenant un terme comme argument. Les clauses "with" et les variantes "e" sont aussi acceptÃ©es. Aussi, discriminate sans argument essaie maintenant toutes les hyps quantifiÃ©es (au lieu de traiter seulement les buts t1<>t2). --This line, and those below, will be ignored-- M doc/refman/RefMan-tac.tex M CHANGES M pretyping/evd.ml M pretyping/termops.ml M pretyping/termops.mli M pretyping/clenv.ml M tactics/extratactics.ml4 M tactics/inv.ml M tactics/equality.ml M tactics/tactics.mli M tactics/equality.mli M tactics/tacticals.ml M tactics/eqdecide.ml4 M tactics/tacinterp.ml M tactics/tactics.ml M tactics/extratactics.mli M toplevel/auto_ind_decl.ml M contrib/funind/invfun.ml M test-suite/success/Discriminate.v M test-suite/success/Injection.v M proofs/clenvtac.mli M proofs/clenvtac.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11159 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extension syntaxique de rewrite in: au lieu de pouvoir faire	letouzey	2006-05-02
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	juste rewrite in <id>, on a maintenant rewrite in <clause>. Ainsi rewrite H in H1,H2 \|- * === rewrite H in H1; rewrite H in H2; rewrite H Pour l'instant rewrite H in * \|- signifie: faire une fois "try rewrite H in Hi" sur toutes les hypotheses Hi du contexte sauf H En particulier, n'echoue pour l'instant pas s'il n'y a rien a reecrire nulle part. NB: rewrite H in * === rewrite H in * \|- * === rewrite H in * \|- ; rewrite H ATTENTION: la syntaxe de rewrite ayant changé, j'adapte interface en conséquence. Est-ce la bonne facon de faire ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8780 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Réintroduction d'un parseur de pattern (q_constr.ml4) à usage de	herbelin	2006-03-22
\| \| \| \| \| \| \| \| \| \| \|	la compilation de fichiers comme hipattern.ml (renommé en hipattern.ml4) - Extension de eqdecide.ml4 pour qu'il gère les buts sans quantificateurs, basés soient sur sumbool soit sur or, et à symétrie près de la disjunction. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8652 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
*	Suppression des parseurs et printeurs v7; suppression du traducteur ↵	herbelin	2005-12-26
\| \| \| \| \| \|	(mécanismes de renommage des noms de constantes, de module, de ltac et de certaines variables liées de lemmes et de tactiques, mécanisme d'ajout d'arguments implicites, etc.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7732 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Types inductifs parametriques	mohring	2005-11-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7493 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
*	Restructuration des procédures de filtrage	herbelin	2003-05-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4032 85f007b7-540e-0410-9357-904b9bb8a0f7
*	simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = ↵	letouzey	2003-04-16
\| \| \| \| \| \|	list_skipn n l git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3931 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
*	Repercussion de la possibilit de mettre des hyps quantifiees dans ↵	herbelin	2002-06-05
\| \| \| \| \| \|	Simplify_eq et Injection git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2757 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Rpercussion de la possibilit de mettre des hyps quantifies dans Simplify_eq ↵	herbelin	2002-06-05
\| \| \| \| \| \|	et Injection git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2754 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fichiers tactics/.ml4 remplacent les tactics/.v	herbelin	2002-05-29
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2719 85f007b7-540e-0410-9357-904b9bb8a0f7