aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* No parentheses around f in 'f \subst{...}'Gravatar herbelin2005-05-26
* Utilisation du module Buffer; encodage plus rigoureux des symboles en uriGravatar herbelin2005-05-26
* Correction of a bug in functional scheme. It raised with mutualGravatar coq2005-05-26
* Patch to avoid Whelp bug removed.Gravatar sacerdot2005-05-26
* Add a guard for V7 mode, CVS compiles cleanly again :)Gravatar coq2005-05-26
* New environment variable COQREMOTEBROWSER to set the command used by CoqGravatar sacerdot2005-05-26
* majGravatar coq2005-05-25
* Forgot to remove a cmo.Gravatar coq2005-05-25
* Added subtac contrib.Gravatar coq2005-05-25
* majGravatar coq2005-05-24
* majGravatar coq2005-05-24
* Added clenv_environments_evars that behaves as clen_environments butGravatar sacerdot2005-05-24
* New commit to allow definitions of morphisms on relations whose carrier isGravatar sacerdot2005-05-24
* WARNING: unification changed (to fix a bug).Gravatar sacerdot2005-05-24
* dp: ajout du prouveur ZenonGravatar coq2005-05-24
* majGravatar coq2005-05-23
* Consequence of allowing the numerical argument of auto to be an ident for ltacGravatar herbelin2005-05-23
* Bug fix for a bug reported by Roland: the function that detects the constantsGravatar sacerdot2005-05-23
* majGravatar coq2005-05-22
* majGravatar coq2005-05-21
* majGravatar coq2005-05-20
* majGravatar coq2005-05-20
* New command: "Print Ltac qualid" to print user defined tactics.Gravatar sacerdot2005-05-20
* Adoption du nom canonique global_of_constr pour éviter confusion avec type r...Gravatar herbelin2005-05-20
* Déplacement et export de locate_global (ex-locate_reference) de tacinterp ve...Gravatar herbelin2005-05-20
* Déplacement et export de locate_global (ex-locate_reference) de tacinterp ve...Gravatar herbelin2005-05-20
* Interface vers outil de recherche WhelpGravatar herbelin2005-05-20
* Adoption du nom canonique global_of_constr pour éviter confusion avec type r...Gravatar herbelin2005-05-20
* DocumentationGravatar herbelin2005-05-20
* Achèvement du déplacement de fonctionnalités unix et browser de ide vers libGravatar herbelin2005-05-20
* majGravatar coq2005-05-19
* majGravatar coq2005-05-19
* DocumentationGravatar herbelin2005-05-19
* Déplacement de fonctionnalités unix et browser de ide vers libGravatar herbelin2005-05-19
* Setoid_replace: improved error message when trying to replace a term in aGravatar sacerdot2005-05-19
* A wish by Bas Spitters granted: a little more of unification up toGravatar sacerdot2005-05-19
* added VernacBacktrack (new backtracking command dedicated toGravatar coq2005-05-19
* majGravatar coq2005-05-18
* majGravatar coq2005-05-18
* Implemented autorewrite with ... in hyp [using ...].Gravatar sacerdot2005-05-18
* majGravatar coq2005-05-17
* majGravatar coq2005-05-17
* Affinements suite à extension Tactic Notation aux tacticiellesGravatar herbelin2005-05-17
* Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...Gravatar herbelin2005-05-17
* Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...Gravatar herbelin2005-05-17
* majGravatar coq2005-05-16
* majGravatar coq2005-05-15
* majGravatar coq2005-05-15
* Globalisation des Tactic NotationGravatar herbelin2005-05-15
* Allow auto to have a parametric argument (wish #967)Gravatar herbelin2005-05-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 23:41:51 +0000