aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/command.mli
Commit message (Expand)AuthorAge
...
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Amelioration dans FunctionGravatar jforest2010-07-16
* change the flag "internal" in declare/ind_tables from bool toGravatar vsiles2010-06-29
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Automatic introduction of names given before ":" in Lemma's andGravatar herbelin2010-06-09
* Fix treatment of {struct x} annotations in presence of generalizedGravatar msozeau2010-06-08
* Various minor improvements of comments in mli for ocamldocGravatar letouzey2010-04-29
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Added support for definition of fixpoints using tactics.Gravatar herbelin2009-11-27
* Added support for multiple where-clauses in Inductive and co (see wish #2163).Gravatar herbelin2009-11-11
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Backtrack on the forced discharge of type class variables introducedGravatar msozeau2009-09-14
* Fix implicit args code so that declarations are added for allGravatar msozeau2009-05-27
* Fix to my last notation patch: now fixpoint are correctly handled Gravatar vsiles2009-05-13
* Fixed bugs #2001 (search_guard was overwriting the guard index givenGravatar herbelin2009-01-04
* More factorization of inductive/record and typeclasses: move classGravatar msozeau2008-11-09
* Nouvelle syntaxe pour écrire des records (co)inductifs :Gravatar aspiwack2008-11-05
* Add enough information to correctly globalize recursive calls in inductive andGravatar msozeau2008-09-11
* Fix bug #1913, checking for unresolved evars which aren't obligations.Gravatar msozeau2008-07-24
* Improvements on coqdoc by adding more information into .globGravatar msozeau2008-05-30
* Postpone the search for the recursive argument index from the user givenGravatar msozeau2008-05-06
* Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuveGravatar herbelin2008-04-25
* Add the ability to specify the implicit status of section variables andGravatar msozeau2008-04-02
* Ajout d'abbréviations/notations paramétriquesGravatar herbelin2008-03-30
* Fix a bug found by B. Grégoire when declaring morphisms in moduleGravatar msozeau2008-03-23
* Do a second pass on the treatment of user-given implicit arguments. NowGravatar msozeau2008-03-15
* Proper implicit arguments handling for assumptionsGravatar msozeau2008-02-26
* Merge with lmamane's private branch:Gravatar lmamane2008-02-22
* Backport Program Instance into Instance. Proper early error message ifGravatar msozeau2008-02-10
* Backport code from command.ml to subtac_command.ml for defininingGravatar msozeau2008-02-08
* Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...Gravatar msozeau2007-12-31
* Modification of the Scheme command.Gravatar vsiles2007-09-28
* Modification of VernacScheme to handle a new scheme: Equality (equality inGravatar vsiles2007-05-25
* New keyword "Inline" for Parameters and Axioms for automatic Gravatar soubiran2007-04-25
* Support for implicit formal argument types in Program ; parse types in type s...Gravatar msozeau2007-03-28
* Add a parameter to QuestionMark evar kind to say it can be turned into an obl...Gravatar msozeau2007-03-19
* Addition of a "Combined Scheme" vernacular command for building the conjuncti...Gravatar msozeau2006-12-23
* Ajout possibilité clause "where" dans co-points fixes Gravatar herbelin2006-09-01
* Restructuration des points d'entrée de Pretyping et ConstrinternGravatar herbelin2005-12-21
* Types inductifs parametriquesGravatar mohring2005-11-02
* Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant dan...Gravatar herbelin2005-01-02
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* Nouvelle en-têteGravatar herbelin2004-07-16
* Export de l'information si un inductive est un record ou non (pour xml)Gravatar herbelin2004-03-31
* Réutilisation de VernacSyntacticDefinition pour différencier "Notation id :...Gravatar herbelin2004-01-29
* Reflet dans l'arbre de syntaxe de la difference syntaxique entre 'Variables a...Gravatar herbelin2004-01-13
* meilleure presentation des commentaires du traducteurGravatar barras2004-01-02
* Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé in...Gravatar herbelin2003-10-08
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 11:30:13 +0000