coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Export Sumbool dans ProbBool; Reals charge et exporte ZArith_base seulement	filliatr	2002-06-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2802 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ZArith_base, Zbool, Bool_nat	filliatr	2002-06-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2798 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Reparation de ring pour les setoides	clrenard	2002-06-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2797 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ProgWf -> Zwf	filliatr	2002-06-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2796 85f007b7-540e-0410-9357-904b9bb8a0f7
*	deplacement contrib/correctness/ProgWf -> theories/ZArith/Zwf	filliatr	2002-06-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2795 85f007b7-540e-0410-9357-904b9bb8a0f7
*	extraction vers scheme	letouzey	2002-06-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2771 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout d'extensions de syntaxe ARGUMENT EXTEND et VERNAC ARGUMENT EXTEND; ↵	herbelin	2002-06-05
\| \| \| \| \| \|	rparation de la protection contre les clauses indiscernables de TACTIC EXTEND et VERNAC COMMAND EXTEND; rparation des grammaires de Extraction, EAuto, TextMode, KillProof et Derive Dependent Inversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2753 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Intgration uniforme de coercions dans les dclarations (Variable and co) et ↵	herbelin	2002-06-03
\| \| \| \| \| \|	retouche des Record git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2747 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Protection des tactiques contre l'utilisation sans le bon contexte de thories	herbelin	2002-06-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2745 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Factorisation de 'Show Programs' au premier niveau de Vernac_.command	herbelin	2002-06-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2744 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵	herbelin	2002-05-29
\| \| \| \| \| \|	commandes vernaculaires (cf dev/changements.txt pour plus de précisions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2734 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fichiers contrib//.ml4 remplacent les contrib//.v	herbelin	2002-05-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2725 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵	herbelin	2002-05-29
\| \| \| \| \| \|	commandes vernaculaires (cf dev/changements.txt pour plus de précisions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2722 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fichiers contrib//.ml4 remplacent les contrib//.v	herbelin	2002-05-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2720 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- abstract_sum_scalar, plus_sum_scalar and minus_sum_scalar were bogus	barras	2002-05-15
\| \| \| \| \| \| \| \|	(did not return an ordered list of monomials). - improved unary negation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2692 85f007b7-540e-0410-9357-904b9bb8a0f7
*	petit bug dans les noms de fichiers	letouzey	2002-04-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2662 85f007b7-540e-0410-9357-904b9bb8a0f7
*	un thm de plus dans Zdiv; un retour chariot apres un message de la tactique ↵	filliatr	2002-04-19
\| \| \| \| \| \|	FourierR git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2659 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	letouzey	2002-04-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2657 85f007b7-540e-0410-9357-904b9bb8a0f7
*	jLogic.mli remplace par jolic.mli	herbelin	2002-04-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2652 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Uniformisation (Qed/Save et Implicits Arguments)	herbelin	2002-04-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2651 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Refine the procedure that generalizes context to current goal.	huang	2002-04-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2646 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj doc extraction dans repertoire contrib/extraction	letouzey	2002-04-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2643 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj test des reals	letouzey	2002-04-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2636 85f007b7-540e-0410-9357-904b9bb8a0f7
*	petit bug avec dummy_lams	letouzey	2002-04-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2635 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
*	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
*	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
*	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
*	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
*	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 *	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
*	- 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
*	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
*	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
*	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
*	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
*	reparation du test des reals	letouzey	2002-03-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2561 85f007b7-540e-0410-9357-904b9bb8a0f7
*	considerations de pretty-print	letouzey	2002-03-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2558 85f007b7-540e-0410-9357-904b9bb8a0f7
*	deux fichiers supplementaires de customisation d'extraction	letouzey	2002-03-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2557 85f007b7-540e-0410-9357-904b9bb8a0f7
*	changement du test extraction suite aux modif inining	letouzey	2002-03-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2556 85f007b7-540e-0410-9357-904b9bb8a0f7
*	modification de l'auto-inlining	letouzey	2002-03-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2555 85f007b7-540e-0410-9357-904b9bb8a0f7
*	renversement du renommage des variables	letouzey	2002-03-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2552 85f007b7-540e-0410-9357-904b9bb8a0f7
*	reparation du controle de l'apparition des termes	letouzey	2002-03-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2551 85f007b7-540e-0410-9357-904b9bb8a0f7
*	reorganisation des simplifications: letin eta-expansé apres le kill-dummy	letouzey	2002-03-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2550 85f007b7-540e-0410-9357-904b9bb8a0f7
*	un peu moins d'eta-expansion autour des Glob	letouzey	2002-03-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2549 85f007b7-540e-0410-9357-904b9bb8a0f7
*	bug optimize_fix fait trop tot	letouzey	2002-03-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2548 85f007b7-540e-0410-9357-904b9bb8a0f7
*	suite bug Dglob constant	letouzey	2002-03-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2547 85f007b7-540e-0410-9357-904b9bb8a0f7