coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	- Changement de l'ordre de filtrage dans "Match Context"	herbelin	2002-05-14
\| \| \| \| \| \| \| \| \| \| \|	- Protection des "Match Context" contre les exceptions non UserError ni Fail - Remplacement des fermetures ML dans VTactic et VFTactic par des expressions de tactiques pour permettre l'intégration de Tactic Definition dans les états - Changement en conséquence de Tauto git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2685 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ajout des theoremes eqT_rec_r et eqT_rect_r pour Rewrite	barras	2002-05-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2680 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Changement de eq en eqT comme equivalence de setoide par defaut.	clrenard	2002-05-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2679 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Minor correction of get_lem_name	coq	2002-05-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2664 85f007b7-540e-0410-9357-904b9bb8a0f7
*	nettoyage code	courant	2002-05-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2663 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
*	* 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
*	- 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
*	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
*	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
*	Intuition ne fait plus de Unfold des constantes (il faut les faire	courant	2002-03-21
\| \| \| \| \| \| \| \|	soi-même si nécessaire) : l'idée est d'avoir un comportement clair et toujours aussi rapide que possible. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2559 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Intuition now takes an (optional) tactic as parameter. This tactic is	courant	2002-03-20
\| \| \| \| \| \| \| \|	used to solve the goal remaining after propositional destructuration of the goal and the hypotheses. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2554 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Tauto est maintenant stable par "Intro" :	courant	2002-03-15
\| \| \| \| \| \| \| \| \| \| \| \|	Tauto montre (x:nat)(P x) \|- (x:nat)(P x) aussi bien que \|- (x:nat)(P x)->(P x) Intuition aussi. De plus, Intuition résout maintenant tout ce que Tauto sait résoudre ; par exemple (A,B,C:Prop)A\/(B/\C->C/\B) (ce qui n'était pas le cas jusqu'ici). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2533 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	mohring	2002-03-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2528 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Simplify_eq echouait sur des hypotheses trivial comme O=O	barras	2002-03-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2518 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	barras	2002-03-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2516 85f007b7-540e-0410-9357-904b9bb8a0f7
*	assert failure avec Conditional Rewrite	barras	2002-03-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2513 85f007b7-540e-0410-9357-904b9bb8a0f7
*	suppression de code mort	barras	2002-03-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2510 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouveau Rewrite-in plus economique	barras	2002-03-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2507 85f007b7-540e-0410-9357-904b9bb8a0f7
*	labels appliques dans un ordre incorrect	barras	2002-03-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2504 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Uniformisation convert_hyp; correction problème de dépendance dans letin_tac	herbelin	2002-02-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2501 85f007b7-540e-0410-9357-904b9bb8a0f7
*	suppression de pop_named	barras	2002-02-22
\| \| \| \| \| \| \|	meilleure discrimination dans les tactiques d'inversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2491 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Elim dependente n'appelait pas la bonne fonction pour calculer le predicat	barras	2002-02-19
\| \| \| \| \| \| \|	d'elimination (d'ou le bug avec Dependent Inversion) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2484 85f007b7-540e-0410-9357-904b9bb8a0f7
*	but de CutRewrite <- (assert false)	barras	2002-02-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2482 85f007b7-540e-0410-9357-904b9bb8a0f7
*	petits changements cosmetiques sur les tactiques	barras	2002-02-15
\| \| \| \| \| \| \| \|	+ Clear independant de l'ordre des hypotheses, et substituant les hypotheses definies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2481 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Reforme de la gestion des args recursifs (via arbres reguliers)	barras	2002-02-14
\| \| \| \| \| \| \|	- coqtop -byte -opt bouclait! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2475 85f007b7-540e-0410-9357-904b9bb8a0f7
*	substitution et pattern modulo let	barras	2002-02-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2466 85f007b7-540e-0410-9357-904b9bb8a0f7
*	mauvais comportement de l'inversion vis-a-vis des lets	barras	2002-02-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2464 85f007b7-540e-0410-9357-904b9bb8a0f7
*	petit nettoyage de kernel/inductive	barras	2002-02-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2460 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout tactiques Rename et Pose; modifications pour Inversion	herbelin	2002-02-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2449 85f007b7-540e-0410-9357-904b9bb8a0f7
*	changement generation de schema d'elimination, False_rec est primitif, ↵	mohring	2002-01-31
\| \| \| \| \| \|	Constructor tac git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2447 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remplacement cut_intro par true_cut_anon pour Inversion	herbelin	2002-01-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2434 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug calcul de la signature incorrecte en présence de letin	herbelin	2002-01-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2433 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remplacement cut_intro par true_cut_anon	herbelin	2002-01-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2431 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug calcul de la signature incorrecte en présence de letin	herbelin	2002-01-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2430 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug dépendances en les corps des let-in oubliées	herbelin	2002-01-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2427 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise de Intros id au format de Intro en forçant aussi la réduction si demandé	herbelin	2002-01-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2397 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise en place de la réduction sous forme d'implications d'atomes en fn de tête	herbelin	2001-12-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2356 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Utilisation de Hnf plutôt que Red	herbelin	2001-12-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2355 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Puisque Orelse semble lier moins que THEN, ajout d'un reduce après le Orelse	herbelin	2001-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2352 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Insertion de Red sur chaque atome dans Tauto et Intuition	herbelin	2001-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2347 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Tentative d'amélioration du résultat de Intuition	herbelin	2001-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2340 85f007b7-540e-0410-9357-904b9bb8a0f7
*	coq-bugs #12: probleme de metamap resolu	barras	2001-12-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2308 85f007b7-540e-0410-9357-904b9bb8a0f7
*	compat ocaml 3.03	filliatr	2001-12-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2291 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Parade contre effet indésirable du commit précédent	herbelin	2001-12-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2277 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Amélioration nommage hypothèses NewInduction (et incompatibilités)	herbelin	2001-12-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2275 85f007b7-540e-0410-9357-904b9bb8a0f7
*	desobfuscation du code de la verif de la condition de garde	barras	2001-11-30
\| \| \| \| \| \| \|	reparation bug de la tactique CutRewrite git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2261 85f007b7-540e-0410-9357-904b9bb8a0f7
*	nouvel algo de conversion plus uniforme	barras	2001-11-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2246 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fusion de declare/add_constant, declare/add_parameter et add_discharged_constant	herbelin	2001-11-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2211 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Diverses petites simplications de la machine de preuves.	clrenard	2001-11-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2204 85f007b7-540e-0410-9357-904b9bb8a0f7