coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	inclusion de meta_map dans evar_defs	barras	2004-09-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6099 85f007b7-540e-0410-9357-904b9bb8a0f7
*	simplification de clenv	barras	2004-09-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6096 85f007b7-540e-0410-9357-904b9bb8a0f7
*	unification encore...	barras	2004-09-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6085 85f007b7-540e-0410-9357-904b9bb8a0f7
*	deuxieme vague de modifs: evar_defs fonctionnel	barras	2004-09-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6071 85f007b7-540e-0410-9357-904b9bb8a0f7
*	premiere reorganisation de l\'unification	barras	2004-09-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6057 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
*	Bug mauvais sigma	herbelin	2004-05-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5735 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Distinction entre declarations internes (p.ex. _subproof) et declarations ↵	herbelin	2004-03-30
\| \| \| \| \| \|	utilisateurs pour export xml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5609 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouvelle reparation pour Abstract en presence de variables de contexte: on ↵	herbelin	2004-03-15
\| \| \| \| \| \|	considere une var de but comme var de contexte si elle a meme nom, meme type, et, le cas echeant meme corps git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5487 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Backtrack sur la réparation de Abstract qui casse autre chose; le problème ↵	herbelin	2004-03-13
\| \| \| \| \| \|	en présence de variables de section est plus subtil et sa résolution est reportée git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5473 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ne pas ajouter le contexte de section dans Abstract, il est deja inclus ↵	herbelin	2004-03-12
\| \| \| \| \| \|	(avec possibles modifications par clear) dans le contexte de but git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5468 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
*	Correction sur commit précédent : Tactics.cut réduisait de manière ↵	herbelin	2004-03-01
\| \| \| \| \| \|	inappropriée git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5409 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Déplacement définition intro_pattern_expr dans Genarg	herbelin	2004-03-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5404 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug (destruct/induction ne savent pas traiter le cas non atomique avec ↵	herbelin	2004-01-27
\| \| \| \| \| \|	paramètres) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5252 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug induction lors de types inductives avec parametres	herbelin	2004-01-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5241 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
*	Reparation incompatibilites v7/v8 dans destruct; utilisation de noms t2_3 ↵	herbelin	2003-12-23
\| \| \| \| \| \|	dans induction/destruct qui marche maintenant git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5137 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
*	Bug introduit avec le 'Simpl f'	herbelin	2003-11-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4971 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug nommage destruct	herbelin	2003-11-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4922 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Move des hyps de NewInduction: retour a situation V7.4 a defaut d'etre robuste	herbelin	2003-11-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4916 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
*	Idtac peut prendre un argument à afficher	narboux	2003-11-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4863 85f007b7-540e-0410-9357-904b9bb8a0f7
*	petits changements de syntaxe	barras	2003-11-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4860 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
*	'NewDestruct using' s'applique maintenant aussi aux types non inductifs; bug ↵	herbelin	2003-11-09
\| \| \| \| \| \|	de Generalize Dependent git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4834 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug Abstract en presence de LetIn; essai d'un Assumption d'abord avec ↵	herbelin	2003-10-21
\| \| \| \| \| \|	alpha-conversion et seulement apres avec conversion (suggestion de Carlos Simpson) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4686 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Deplacement next_global_ident_away dans Termops	herbelin	2003-10-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4605 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Typo	herbelin	2003-10-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4581 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout option 'as [ ... ]' pour nommer les noms de 'Inversion'	herbelin	2003-10-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4580 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
*	Correction bug NewInduction pour les inductifs de type 'ordinaux'	herbelin	2003-09-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4462 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Indépendance vis à vis de Declare	herbelin	2003-09-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4372 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
*	Backtrack du commit de Christine, qui posait probleme avec FTC	letouzey	2003-04-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3842 85f007b7-540e-0410-9357-904b9bb8a0f7
*	notations <>, Assumption avec existentiel, replace term	mohring	2003-03-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3802 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Un type "standardisé" pour new_hyp	herbelin	2003-01-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3611 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Commentaires; optimisation	herbelin	2002-12-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3486 85f007b7-540e-0410-9357-904b9bb8a0f7
*	code mort	herbelin	2002-12-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3481 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
*	Normalisation beta-iota du type du terme appliqué (fait avant dans Typing)	herbelin	2002-12-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3417 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
*	JMeq now treated as an equality by tactics.	courant	2002-11-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3232 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Intégration des modifs de la branche mowgli :	herbelin	2002-11-05
\| \| \| \| \| \| \| \| \| \| \|	- Simplification de strength qui est maintenant un simple drapeau Local/Global. - Export des catégories de déclarations (Lemma/Theorem/Definition/.../ Axiom/Parameter/..) vers les .vo (nouveau fichier library/decl_kinds.ml). - Export des variables de section initialement associées à une déclaration (nouveau fichier library/dischargedhypsmap.ml). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3212 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction d'une incompatibilité de nommage introduite lors du commit ↵	herbelin	2002-10-22
\| \| \| \| \| \|	précédent git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3171 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