aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/interface
Commit message (Expand)AuthorAge
* New command: "Print Ltac qualid" to print user defined tactics.Gravatar sacerdot2005-05-20
* added VernacBacktrack (new backtracking command dedicated toGravatar coq2005-05-19
* Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...Gravatar herbelin2005-05-17
* Allow auto to have a parametric argument (wish #967)Gravatar herbelin2005-05-15
* Added 'clear - id' to clear all hypotheses except the ones dependent in the s...Gravatar herbelin2005-03-07
* Renaming Print Canonical Structure into Print Canonical ProjectionsGravatar herbelin2005-02-18
* Standardisation of function names about global references (especially, renami...Gravatar herbelin2005-02-18
* Ajout Print Canonical StructuresGravatar herbelin2005-02-12
* Nettoyage et documentation de LibraryGravatar herbelin2005-02-06
* Ajout cas VernacBackToGravatar herbelin2005-01-26
* Construct "T with (Definition|Module) id := c" generalized toGravatar sacerdot2005-01-13
* - Module/Declare Module syntax made more uniform:Gravatar sacerdot2005-01-06
* Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...Gravatar herbelin2004-12-24
* Restauration type casted_open_constr pour tactique refine car l'unification n...Gravatar herbelin2004-12-09
* * added subst_evaluable_referenceGravatar sacerdot2004-12-07
* Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des tacti...Gravatar herbelin2004-12-06
* Correction 1.138 appliquée à tort à la branche principale au lieu de V8-0b...Gravatar herbelin2004-11-29
* Commit précédent erroné; retour version précédenteGravatar herbelin2004-11-29
* MAJ vis à vis de extratacticsGravatar herbelin2004-11-28
* Locate ModuleGravatar herbelin2004-11-17
* New command "Print Rewrite HindDb dbname".Gravatar sacerdot2004-11-17
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* 'match term' now evaluates by default. Added 'lazy' keyword to delay the eval...Gravatar herbelin2004-10-11
* restructuration des printers: proofs passe avant parsingGravatar barras2004-09-17
* Ajout de or-pattern pour le match-with v8Gravatar herbelin2004-09-09
* premiere reorganisation de l\'unificationGravatar barras2004-09-03
* "Show Setoids" command added.Gravatar sacerdot2004-07-23
* Abstraction vis a vis du type loc pour ocaml 3.08Gravatar herbelin2004-07-18
* Nouvelle en-têteGravatar herbelin2004-07-16
* moved instantiate binding to extratacticsGravatar corbinea2004-06-29
* License de contrib/interfaceGravatar herbelin2004-06-29
* contrib/interface *$*$@!Gravatar corbinea2004-06-28
* pb install de pcoqGravatar barras2004-04-21
* preparation pour release (suite)Gravatar barras2004-03-15
* To make that the translation process does not fail on data produced byGravatar bertot2004-03-15
* modif des fixpoints pour que si on donne une notation au produit, les pts fix...Gravatar barras2004-03-05
* takes better account of the new possibility to pass a parametric count argumentGravatar bertot2004-03-03
* removes capital letters in two tactic names.Gravatar bertot2004-03-03
* make sure the implicit argument indications are in the right orderGravatar bertot2004-03-03
* Ajout d'une entrée hyp de type HypArgType pour parser et interpréter les no...Gravatar herbelin2004-03-02
* Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id va...Gravatar herbelin2004-03-02
* Ajout IntroPattern comme type d'argument génériqueGravatar herbelin2004-03-01
* Keep structure information for Fixpoint declaration and Fix termsGravatar bertot2004-02-26
* Not all cases for coercions and locality were handledGravatar bertot2004-02-26
* corrects the treatement of SubClass declarationsGravatar bertot2004-02-23
* makes sure the following examples are well-treated:Gravatar bertot2004-02-19
* - fixed the Assert_failure error in kernel/modopsGravatar barras2004-02-18
* accomodate the .. extensionGravatar bertot2004-02-16
* adds a new command for searching a pattern inside the premises of theoremsGravatar bertot2004-02-16