coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	COMMITED BYTECODE COMPILER	barras	2004-10-20
*	'match term' now evaluates by default. Added 'lazy' keyword to delay the eval...	herbelin	2004-10-11
*	Ajout de or-pattern pour le match-with v8	herbelin	2004-09-09
*	"Show Setoids" command added.	sacerdot	2004-07-23
*	Abstraction vis a vis du type loc pour ocaml 3.08	herbelin	2004-07-18
*	moved instantiate binding to extratactics	corbinea	2004-06-29
*	contrib/interface $$@!	corbinea	2004-06-28
*	preparation pour release (suite)	barras	2004-03-15
*	To make that the translation process does not fail on data produced by	bertot	2004-03-15
*	modif des fixpoints pour que si on donne une notation au produit, les pts fix...	barras	2004-03-05
*	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-03
*	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-02
*	Ajout IntroPattern comme type d'argument générique	herbelin	2004-03-01
*	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-26
*	corrects the treatement of SubClass declarations	bertot	2004-02-23
*	makes sure the following examples are well-treated:	bertot	2004-02-19
*	- fixed the Assert_failure error in kernel/modops	barras	2004-02-18
*	accomodate the .. extension	bertot	2004-02-16
*	adds the possibility to have terms (and not just identifiers) as hints	bertot	2004-02-13
*	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-12
*	adds the possibility to mark function arguments as formulas in Ltac	bertot	2004-02-02
*	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-30
*	Réutilisation de VernacSyntacticDefinition pour différencier "Notation id :...	herbelin	2004-01-29
*	updates the tactics contradiction and autorewrite, the commands	bertot	2004-01-29
*	make sure that 'in' clauses for reduction tactics are translated	bertot	2004-01-28
*	a try to make intro patterns better	bertot	2004-01-26
*	streamlines the keywords for definitions, require commandsbinders, notation	bertot	2004-01-24
*	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	2004-01-22
*	adds the notations in inductive definitions, improves the consistency between	bertot	2004-01-22
*	handles explicit function calls, names meta variables in patterns	bertot	2004-01-22
*	updates the structure of fix (struct argument added) and if	bertot	2004-01-21
*	handles projector notations, cases with return types,	bertot	2004-01-19
*	adds constructs to handle notations in patterns	bertot	2004-01-19
*	translation to structures now okay for pattern matching constructs	bertot	2004-01-15
*	compact nested universal quantifications into a single quantification with	bertot	2004-01-14
*	Reflet dans l'arbre de syntaxe de la difference syntaxique entre 'Variables a...	herbelin	2004-01-13
*	bugs avec Pose et Assert	barras	2004-01-09
*	meilleure presentation des commentaires du traducteur	barras	2004-01-02
*	Nouvelle tactique EExists	clrenard	2003-12-01
*	Uniformisation des politiques de nommage de NewDestruct sur arguments recursi...	herbelin	2003-11-25
*	correction suite ajout nouvelles tactiques	clrenard	2003-11-18
*	Ajout Print Implicit avec depliage du type	herbelin	2003-11-15