aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2005-05-29majcoq
2005-05-28majcoq
2005-05-28unification: evar_define checks the free variables are bound in the evar contextbarras
2005-05-27majcoq
2005-05-26majcoq
2005-05-26No parentheses around f in 'f \subst{...}'herbelin
2005-05-26Utilisation du module Buffer; encodage plus rigoureux des symboles en uriherbelin
2005-05-26Correction of a bug in functional scheme. It raised with mutualcoq
2005-05-26Patch to avoid Whelp bug removed.sacerdot
2005-05-26Add a guard for V7 mode, CVS compiles cleanly again :)coq
2005-05-26New environment variable COQREMOTEBROWSER to set the command used by Coqsacerdot
2005-05-25majcoq
2005-05-25Forgot to remove a cmo.coq
2005-05-25Added subtac contrib.coq
2005-05-24majcoq
2005-05-24majcoq
2005-05-24Added clenv_environments_evars that behaves as clen_environments butsacerdot
2005-05-24New commit to allow definitions of morphisms on relations whose carrier issacerdot
2005-05-24WARNING: unification changed (to fix a bug).sacerdot
2005-05-24dp: ajout du prouveur Zenoncoq
2005-05-23majcoq
2005-05-23Consequence of allowing the numerical argument of auto to be an ident for ltacherbelin
2005-05-23Bug fix for a bug reported by Roland: the function that detects the constantssacerdot
2005-05-22majcoq
2005-05-21majcoq
2005-05-20majcoq
2005-05-20majcoq
2005-05-20New command: "Print Ltac qualid" to print user defined tactics.sacerdot
2005-05-20Adoption du nom canonique global_of_constr pour éviter confusion avec type r...herbelin
2005-05-20Déplacement et export de locate_global (ex-locate_reference) de tacinterp ve...herbelin
2005-05-20Déplacement et export de locate_global (ex-locate_reference) de tacinterp ve...herbelin
2005-05-20Interface vers outil de recherche Whelpherbelin
2005-05-20Adoption du nom canonique global_of_constr pour éviter confusion avec type r...herbelin
2005-05-20Documentationherbelin
2005-05-20Achèvement du déplacement de fonctionnalités unix et browser de ide vers libherbelin
2005-05-19majcoq
2005-05-19majcoq
2005-05-19Documentationherbelin
2005-05-19Déplacement de fonctionnalités unix et browser de ide vers libherbelin
2005-05-19Setoid_replace: improved error message when trying to replace a term in asacerdot
2005-05-19A wish by Bas Spitters granted: a little more of unification up tosacerdot
2005-05-19added VernacBacktrack (new backtracking command dedicated tocoq
2005-05-18majcoq
2005-05-18majcoq
2005-05-18Implemented autorewrite with ... in hyp [using ...].sacerdot
2005-05-17majcoq
2005-05-17majcoq
2005-05-17Affinements suite à extension Tactic Notation aux tacticiellesherbelin
2005-05-17Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...herbelin
2005-05-17Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-20 20:01:38 +0000