coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	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
*	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
*	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
*	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
*	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
*	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
*	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
*	affichages avec prterm_env et non prterm; deb_print pour vraiment ne rien ↵	filliatr	2002-02-08
\| \| \| \| \| \|	faire si pas debug git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2462 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
*	un assert false de trop (MLexn peut avoir des args)	letouzey	2002-02-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2458 85f007b7-540e-0410-9357-904b9bb8a0f7
*	oubli	letouzey	2002-02-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2457 85f007b7-540e-0410-9357-904b9bb8a0f7
*	gros changement dans mlutil.ml: ajout d'une elimination globale des prop	letouzey	2002-02-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2456 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout d'optimisations locales kill_prop	letouzey	2002-02-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2452 85f007b7-540e-0410-9357-904b9bb8a0f7
*	adaptation de l'extraction aux changements de Christine concernant rec/rect ↵	letouzey	2002-01-31
\| \| \| \| \| \|	et False_rec git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2448 85f007b7-540e-0410-9357-904b9bb8a0f7
*	extraction des CoInductives via les Lazy d'ocaml	letouzey	2002-01-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2446 85f007b7-540e-0410-9357-904b9bb8a0f7
*	patch Omega (bug 129)	filliatr	2002-01-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2436 85f007b7-540e-0410-9357-904b9bb8a0f7
*	In Pcoq, the search commands had an erroneous behavior. Bound variables	bertot	2002-01-23
\| \| \| \| \| \| \| \|	in theorems were renamed to avoid the names present in the current goal's context. This version corrects this problem. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2425 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction de Pierre Crégut pour le bug MERGE_EQ	herbelin	2002-01-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2421 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Zinv -> Zopp	filliatr	2002-01-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2419 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug MERGE_EQ	herbelin	2002-01-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2416 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Plusieurs arguments autorisés pour Require et Read Module	herbelin	2002-01-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2412 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ajouts provenant de Chinese dans ZArith + deplacements de 3 fichiers de ↵	letouzey	2002-01-18
\| \| \| \| \| \|	contrib/omega vers theories/ZArith git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2406 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Orthographe	herbelin	2002-01-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2392 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj CHANGES extraction + bug extraction & _	letouzey	2001-12-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2359 85f007b7-540e-0410-9357-904b9bb8a0f7
*	contrib/interface/dad.ml4 had no real need of streams, it should have been	bertot	2001-12-19
\| \| \| \| \| \| \| \|	translated into a regular ml files like the others. This mistake is now corrected. The Makefile and dependency files are updated accordingly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2345 85f007b7-540e-0410-9357-904b9bb8a0f7
*	debranchement du test sur les Reals	letouzey	2001-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2344 85f007b7-540e-0410-9357-904b9bb8a0f7
*	reparation du make depend et du .depend	letouzey	2001-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2334 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Corrections post contournement des streams avec ++	herbelin	2001-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2332 85f007b7-540e-0410-9357-904b9bb8a0f7
*	the function Ctast.section_path was wrong. It performed two reverse	bertot	2001-12-18
\| \| \| \| \| \| \|	operations on lists, which was equivalent to doing nothing. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2320 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Pour ocamlweb ...	letouzey	2001-12-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2319 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Oubli d'un quote	herbelin	2001-12-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2318 85f007b7-540e-0410-9357-904b9bb8a0f7
*	There remained traces of streams with the old syntax.	bertot	2001-12-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2316 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Integrating the Ltac language and the Blast tool into the interface	bertot	2001-12-18
\| \| \| \| \| \| \| \| \| \| \| \| \|	capabilities: The Ltac language is the language that makes it possible to define new tactics without using the ocaml language (already present in coq for a few months). The Blast tool is a tool that checks whether the goals could be solve automatically and proposes the proof trace to the user. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2313 85f007b7-540e-0410-9357-904b9bb8a0f7
*	typo de parenthèsage + suppression de string (= str maintenant)	letouzey	2001-12-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2311 85f007b7-540e-0410-9357-904b9bb8a0f7
*	anti revolution culturelle: retour des arguments logiques	letouzey	2001-12-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2310 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ote les redondances des entetes	letouzey	2001-12-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2309 85f007b7-540e-0410-9357-904b9bb8a0f7
*	le save de Correctness faisant assert false	barras	2001-12-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2300 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
*	correction de bugs concernant la gestion des modules. debranchement du test ↵	letouzey	2001-12-10
\| \| \| \| \| \|	d'extraction sur les Reals en attendant git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2282 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
*	remise au gout du jour du repertoire theories/Sorting de la V6.3	letouzey	2001-11-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2231 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Make sure that NatRing won't loop forever.	bertot	2001-11-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2226 85f007b7-540e-0410-9357-904b9bb8a0f7
*	hack temporaire concernant les remarks/modules	letouzey	2001-11-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2217 85f007b7-540e-0410-9357-904b9bb8a0f7