coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Deuxième passe sur la localisation des messages d'erreurs sur les evars non ↵	herbelin	2002-04-11
\| \| \| \| \| \|	définies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2633 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Factorisation de quelques fonctions de clenv.ml; code mort dans coq_omega.ml	herbelin	2002-04-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2632 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Simplification du nom de l'architecture Mac OS X	herbelin	2002-04-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2631 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Amélioration des messages d'erreurs concernant l'inférence des implicites	herbelin	2002-04-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2630 85f007b7-540e-0410-9357-904b9bb8a0f7
*	backtrack dans l'algo d'unification	barras	2002-04-10
\| \| \| \| \| \| \|	fichier usage incorrect (libdir et bindir ont disparu) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2629 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Syntactic Definition autorisée dans les motifs de Cases (utile notamment	herbelin	2002-04-10
\| \| \| \| \| \| \|	pour fusionner eq et eqT) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2628 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2002-04-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2627 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Simplification des Clear internes dégénérés (sans hypothèses à effacer)	herbelin	2002-04-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2626 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2002-04-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2625 85f007b7-540e-0410-9357-904b9bb8a0f7
*	package camlindent inutilise	barras	2002-04-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2624 85f007b7-540e-0410-9357-904b9bb8a0f7
*	extraction.ml	letouzey	2002-04-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2623 85f007b7-540e-0410-9357-904b9bb8a0f7
*	babioles de renommages	letouzey	2002-04-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2622 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Zdiv -> Export ZArith	filliatr	2002-04-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2621 85f007b7-540e-0410-9357-904b9bb8a0f7
*	syntaxe pour Zdiv et Zmod	filliatr	2002-04-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2620 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ajout du mange-tout d'argument en ocaml + error en Haskell pour la constante ↵	letouzey	2002-04-08
\| \| \| \| \| \|	dummy git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2619 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	courant	2002-04-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2618 85f007b7-540e-0410-9357-904b9bb8a0f7
*	export de la fonction Reductionops.find_conclusion pour l'extraction	letouzey	2002-04-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2617 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression de l'application de f_equal2 pour "mult" (non inversible);	herbelin	2002-04-05
\| \| \| \| \| \| \| \|	Application de f_equal2 pour "plus" seulement si soit les membres droits soit les membres gauches sont égaux. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2616 85f007b7-540e-0410-9357-904b9bb8a0f7
*	simplification preuve	filliatr	2002-04-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2615 85f007b7-540e-0410-9357-904b9bb8a0f7
*	nouveau module Zdiv	filliatr	2002-04-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2614 85f007b7-540e-0410-9357-904b9bb8a0f7
*	mise jour	filliatr	2002-04-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2613 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	mohring	2002-04-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2612 85f007b7-540e-0410-9357-904b9bb8a0f7
*	meilleure gestion du point terminal	filliatr	2002-04-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2611 85f007b7-540e-0410-9357-904b9bb8a0f7
*	resolution du pb d'efficacite du a Sign.add_named_decl	barras	2002-04-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2610 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added credits for jprover.	huang	2002-04-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2609 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	huang	2002-04-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2608 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add citations	huang	2002-04-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2607 85f007b7-540e-0410-9357-904b9bb8a0f7
*	renommage de l'exception locale Arity	barras	2002-04-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2606 85f007b7-540e-0410-9357-904b9bb8a0f7
*	transformation des evar en meta preserve la linearite des metas	barras	2002-04-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2605 85f007b7-540e-0410-9357-904b9bb8a0f7
*	changement de l'undo limit	barras	2002-04-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2604 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Optimisation	desmettr	2002-04-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2582 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression PI_lb et PI_ub	desmettr	2002-04-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2581 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression Field	desmettr	2002-04-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2580 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- modifs de la condition de garde pour mieux tenir compte des raisonnements	barras	2002-04-02
\| \| \| \| \| \| \| \| \| \|	par l'absurde - un open_constr est maintenant un terme accompagne du sigma dans lequel il est typable (il manquait l'info concernant le contexte de typage des nouvelles evars) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2579 85f007b7-540e-0410-9357-904b9bb8a0f7
*	sans utiliser Field	desmettr	2002-03-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2578 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction bug infix sur des varaiables	mohring	2002-03-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2577 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	mohring	2002-03-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2576 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression des invocations a Field	desmettr	2002-03-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2575 85f007b7-540e-0410-9357-904b9bb8a0f7
*	reparation du cas des arguments de type qui sont des arités + patch dummy ↵	letouzey	2002-03-28
\| \| \| \| \| \|	applied git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2574 85f007b7-540e-0410-9357-904b9bb8a0f7
*	petite erreur dans le typage des let-in	barras	2002-03-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2573 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug d'affichage des erreurs localisées dans un fichier suite à	herbelin	2002-03-27
\| \| \| \| \| \| \|	changement de précédence de ++, anciennement [< ; >], vis à vis du if git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2572 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Simplification de Proof_type.prim_rule	herbelin	2002-03-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2571 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Elimination Elimdep.v	mohring	2002-03-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2570 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	mohring	2002-03-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2569 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Refonte complete de la génération des types ML	letouzey	2002-03-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2568 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Prise en compte des dependances dans la tactique Case	mohring	2002-03-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2567 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	werner	2002-03-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2566 85f007b7-540e-0410-9357-904b9bb8a0f7
*	code redondant	herbelin	2002-03-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2565 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug d'affichage des réels dû à une collision entre les APPLINSIDETAIL de ↵	herbelin	2002-03-22
\| \| \| \| \| \|	Zsyntax et de Rsyntax (dont les règles ne s'appliquent plus dans le même ordre depuis la modification de l'ordre de chargement des Require) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2564 85f007b7-540e-0410-9357-904b9bb8a0f7
*	An intuitionistic first-order theorem prover -- JProver.	huang	2002-03-22
\| \| \| \| \| \| \|	See the "README" file for more information. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2563 85f007b7-540e-0410-9357-904b9bb8a0f7