aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/topconstr.mli
Commit message (Expand)AuthorAge
* Utilisation de try_locate_qualified_library au lieu de locate_qualified_libra...Gravatar notin2008-07-07
* Fixes in handling of implicit arguments:Gravatar msozeau2008-07-04
* Improvements on coqdoc by adding more information into .globGravatar msozeau2008-05-30
* Ajout de la possibilité d'utiliser fix/cofix dans les notations.Gravatar herbelin2008-05-24
* Postpone the search for the recursive argument index from the user givenGravatar msozeau2008-05-06
* Ajout d'abbréviations/notations paramétriquesGravatar herbelin2008-03-30
* - Second pass on implementation of let pattern. Parse "let ' par [as x]?Gravatar msozeau2008-03-28
* Beaoucoup de changements dans la representation interne des modules.Gravatar soubiran2008-02-01
* Add new LetPattern construct to replace dest. syntax: let| pat := t in b is b...Gravatar msozeau2008-01-17
* Generalize instance declarations to any context, better name handling. Add ho...Gravatar msozeau2008-01-15
* Correction bug #1749 (datant de l'implantation des or-patterns) +Gravatar herbelin2008-01-05
* Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...Gravatar msozeau2007-12-31
* - Débogueur: positionnement de set_detype_anonymous pour ne pasGravatar herbelin2007-08-29
* Add a parameter to QuestionMark evar kind to say it can be turned into an obl...Gravatar msozeau2007-03-19
* Remplacement de la dépendance de G_vernac en G_constr (sourceGravatar herbelin2006-12-03
* Notations:Gravatar herbelin2006-10-09
* Annulation de l'essai de changement de sémantique du %scope (révision 9208).Gravatar herbelin2006-10-06
* Essai de changement de sémantique du %scope : Gravatar herbelin2006-10-05
* Correction bug 1172 + correction en passant de la taille des paramètres de f...Gravatar herbelin2006-07-07
* Extension des motifs disjonctifs au cas de disjonction de motifs multiplesGravatar herbelin2006-07-03
* Added {measure x f} as a valid recursion order.Gravatar msozeau2006-06-22
* The "clean integration of subtac" patch.Gravatar msozeau2006-05-29
* - Distinction explicite des parties paramètres et arguments dans le typeGravatar herbelin2006-04-27
* Si un fixpoint a plusieurs arguments, mais un seul de type inductif, Gravatar letouzey2006-04-14
* Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.Gravatar msozeau2006-03-13
* exporting the global reference to the inductive " \/ " in coqlib andGravatar bertot2006-01-25
* Restructuration et simplification des fonctions d'affichage, de détypageGravatar herbelin2006-01-11
* Suppression redondance coerce_to_id dans Pcoq et constrintern et déplacement...Gravatar herbelin2006-01-09
* Ajout rawconstr_of_aconstrGravatar herbelin2006-01-08
* Ajout d'un mécanisme d'interprétation et d'affichage pour les littéraux de...Gravatar herbelin2005-12-30
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Changement des named_contextGravatar gregoire2005-12-02
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
* Construct "T with (Definition|Module) id := c" generalized toGravatar sacerdot2005-01-13
* HUGE COMMITGravatar sacerdot2005-01-03
* Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...Gravatar herbelin2004-12-25
* Names.substitution (and related functions) and Term.subst_mps moved toGravatar sacerdot2004-11-16
* hiding the meta_map in evar_defsGravatar barras2004-09-15
* Ajout de or-pattern pour le match-with v8Gravatar herbelin2004-09-09
* Nouvelle en-têteGravatar herbelin2004-07-16
* Motifs recursifs de notations: prise en compte de l'associativite et des nota...Gravatar herbelin2004-03-17
* Mise en place de motifs récursifs dans Notation; quelques simplifications au...Gravatar herbelin2004-03-17
* modif des fixpoints pour que si on donne une notation au produit, les pts fix...Gravatar barras2004-03-05
* Keep structure information for Fixpoint declaration and Fix termsGravatar bertot2004-02-26
* - fixed the Assert_failure error in kernel/modopsGravatar barras2004-02-18
* meilleure presentation des commentaires du traducteurGravatar barras2004-01-02
* Distinction entre 'as _' qui cache le terme filtre (si variable) et rien dans...Gravatar herbelin2003-11-19
* Ajout CPatNotation; renommage map_aconstr_with_binders_locGravatar herbelin2003-11-01
* Syntaxe plus liberale pour le type des arguments de filtrage du 'match'Gravatar herbelin2003-09-26
* Mise en place d'implicites par noms en v8Gravatar herbelin2003-09-21