coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	cas des constructeurs singletons. Messages d'erreur. Revision de ↵	letouzey	2002-03-05
\| \| \| \| \| \|	test_extraction.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2514 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
*	petits changements afin de profiter du nouveau Rewrite/in	barras	2002-03-05
\| \| \| \| \| \| \|	(l'unification marche mieux) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2512 85f007b7-540e-0410-9357-904b9bb8a0f7
*	unification faite de gauche a droite (et non pas l'inverse) pour eviter que	barras	2002-03-05
\| \| \| \| \| \| \|	clenv_typed_unify plante trop facilement git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2511 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
*	* empty log message *	barras	2002-03-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2509 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Big commit extraction:	letouzey	2002-03-04
\| \| \| \| \| \| \| \| \| \| \|	- Changement de syntaxe (Extraction Language Toplevel/Ocaml/Haskell) - Retour des inductifs singletons et vides dans extraction.ml (extraction.ml -> actions sur le type, mlutil.ml -> conserve le type) - maintenant par defaut Recursive Extraction === Extraction "file" - kill_prop global est fait dans extraction.ml selon typage (a suivre...) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2508 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
*	Nouveau comportement: Delta ne s'applique pas aux variables liées par un let	herbelin	2002-03-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2506 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Prise en compte des corps de letin dans les hypothèses	herbelin	2002-03-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2505 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
*	convert_hyp a change de type	barras	2002-03-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2503 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Uniformisation convert_hyp	herbelin	2002-02-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2502 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
*	* empty log message *	herbelin	2002-02-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2500 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ajout option_compare	herbelin	2002-02-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2499 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Generalisation de l'utilisation de l'unification d'ordre 2	barras	2002-02-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2498 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout andb_true_eq pour PolyList.list_beq	herbelin	2002-02-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2497 85f007b7-540e-0410-9357-904b9bb8a0f7
*	modifs des preambules d'extraction modulaire	letouzey	2002-02-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2496 85f007b7-540e-0410-9357-904b9bb8a0f7
*	-dump-glob dans le usage	filliatr	2002-02-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2495 85f007b7-540e-0410-9357-904b9bb8a0f7
*	pretty print des Cases devenant des let-in	letouzey	2002-02-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2494 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Doc + ajout fold_symmetric et nth_In	herbelin	2002-02-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2493 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Doc	herbelin	2002-02-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2492 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
*	code mort dans tactinterp; plus de Debug On/Off dans Correctness	filliatr	2002-02-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2490 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Changé le nom du module Errors (errors.mli, errors.ml) en Cerrors parce	ddr	2002-02-20
\| \| \| \| \| \| \| \|	qu'il entre en conflit avec le module Errors ajouté dans OCaml courant (future version OCaml 3.05). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2489 85f007b7-540e-0410-9357-904b9bb8a0f7
*	typage du produit: type_judgment appele avec contexte incorrect	barras	2002-02-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2488 85f007b7-540e-0410-9357-904b9bb8a0f7
*	meilleur message d'erreur lorsqu'on type une evar qui n'existe pas	barras	2002-02-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2487 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Le type des evars transformees en meta n'etait pas normalise, et des Evars	barras	2002-02-19
\| \| \| \| \| \| \|	definies y apparaissait git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2486 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Uniformisation des theoremes dans Set et Type (def. de Acc_rect et	barras	2002-02-19
\| \| \| \| \| \| \|	well_founded_induction_type) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2485 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
*	bug #134: on appelait solve_simple_eqn avec une evar qui etait resolue	barras	2002-02-18
\| \| \| \| \| \| \|	par comparaison de ses arguments git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2483 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
*	suite et fin (?) de haskell: gestion des modules, mise en place du'un test	letouzey	2002-02-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2480 85f007b7-540e-0410-9357-904b9bb8a0f7
*	bootstrap consistent avec les options de la ligne de commande	filliatr	2002-02-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2478 85f007b7-540e-0410-9357-904b9bb8a0f7
*	debut de gestion des open pour extraction modulaire	letouzey	2002-02-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2477 85f007b7-540e-0410-9357-904b9bb8a0f7
*	qq inline manuels (sigS_rec ...) + utilisation de library_part	letouzey	2002-02-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2476 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
*	option -dump-glob pour coqdoc	filliatr	2002-02-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2474 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Syntaxe IF then else au lieu de either and_then or_else	barras	2002-02-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2473 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Raffinement library_part	herbelin	2002-02-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2472 85f007b7-540e-0410-9357-904b9bb8a0f7
*	petite modif pour ne pas expanser trop de let pendant l'unification	barras	2002-02-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2471 85f007b7-540e-0410-9357-904b9bb8a0f7
*	suppression de la condition de la permutation case/fun	letouzey	2002-02-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2470 85f007b7-540e-0410-9357-904b9bb8a0f7
*	pretty print	letouzey	2002-02-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2469 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Test & correction de la production de code Haskell	letouzey	2002-02-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2468 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout library_part	herbelin	2002-02-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2467 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
*	bad printing of Zeta reduction flags (was missing)	barras	2002-02-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2465 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