coq - The formal proof system

Age	Commit message (Expand)	Author
2005-03-07	Added 'clear - id' to clear all hypotheses except the ones dependent in the s...	herbelin
2005-02-18	Renaming Print Canonical Structure into Print Canonical Projections	herbelin
2005-02-12	Ajout Print Canonical Structures	herbelin
2005-01-26	Ajout cas VernacBackTo	herbelin
2005-01-13	Construct "T with (Definition\|Module) id := c" generalized to	sacerdot
2005-01-06	- Module/Declare Module syntax made more uniform:	sacerdot
2004-12-24	Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...	herbelin
2004-12-09	Restauration type casted_open_constr pour tactique refine car l'unification n...	herbelin
2004-12-06	Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des tacti...	herbelin
2004-11-29	Correction 1.138 appliquée à tort à la branche principale au lieu de V8-0b...	herbelin
2004-11-29	Commit précédent erroné; retour version précédente	herbelin
2004-11-28	MAJ vis à vis de extratactics	herbelin
2004-11-17	Locate Module	herbelin
2004-11-17	New command "Print Rewrite HindDb dbname".	sacerdot
2004-10-20	COMMITED BYTECODE COMPILER	barras
2004-10-11	'match term' now evaluates by default. Added 'lazy' keyword to delay the eval...	herbelin
2004-09-09	Ajout de or-pattern pour le match-with v8	herbelin
2004-07-23	"Show Setoids" command added.	sacerdot
2004-07-18	Abstraction vis a vis du type loc pour ocaml 3.08	herbelin
2004-06-29	moved instantiate binding to extratactics	corbinea
2004-06-28	contrib/interface $$@!	corbinea
2004-03-15	preparation pour release (suite)	barras
2004-03-15	To make that the translation process does not fail on data produced by	bertot
2004-03-05	modif des fixpoints pour que si on donne une notation au produit, les pts fix...	barras
2004-03-03	takes better account of the new possibility to pass a parametric count argument	bertot
2004-03-03	removes capital letters in two tactic names.	bertot
2004-03-02	Ajout d'une entrée hyp de type HypArgType pour parser et interpréter les no...	herbelin
2004-03-02	Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id va...	herbelin
2004-03-01	Ajout IntroPattern comme type d'argument générique	herbelin
2004-02-26	Keep structure information for Fixpoint declaration and Fix terms	bertot
2004-02-26	Not all cases for coercions and locality were handled	bertot
2004-02-23	corrects the treatement of SubClass declarations	bertot
2004-02-19	makes sure the following examples are well-treated:	bertot
2004-02-18	- fixed the Assert_failure error in kernel/modops	barras
2004-02-16	accomodate the .. extension	bertot
2004-02-13	adds the possibility to have terms (and not just identifiers) as hints	bertot
2004-02-12	lazy was translated to cbv, obviously wrong	bertot
2004-02-12	Implicits can have an optional list of argument, which is different	bertot
2004-02-02	adds the possibility to mark function arguments as formulas in Ltac	bertot
2004-01-30	updates the definition of tactics using Ltac and adds the subst tactic	bertot
2004-01-30	adds module commands and update the extration command	bertot
2004-01-29	Réutilisation de VernacSyntacticDefinition pour différencier "Notation id :...	herbelin
2004-01-29	updates the tactics contradiction and autorewrite, the commands	bertot
2004-01-28	make sure that 'in' clauses for reduction tactics are translated	bertot
2004-01-26	a try to make intro patterns better	bertot
2004-01-24	streamlines the keywords for definitions, require commandsbinders, notation	bertot
2004-01-22	change add path commands to get the extra argument and the Hint commands	bertot
2004-01-22	fixes argument lists for tactic definitions, updates inversion tactics	bertot
2004-01-22	adds a clause argument to symmetry	bertot
2004-01-22	corrects the way the structural argument declaration is handled in	bertot