aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrintern.ml
Commit message (Expand)AuthorAge
* Postpone the search for the recursive argument index from the user givenGravatar msozeau2008-05-06
* Factorize code for internalization of binders to fix bug #1846. AlsoGravatar msozeau2008-05-04
* Correction bug List.map2 dans Case12.vGravatar herbelin2008-04-09
* Modifications diverses et variées :Gravatar herbelin2008-03-30
* 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
* Various fixes on typeclasses:Gravatar msozeau2008-03-27
* Finish fix in command where we still lost information on what was a typeGravatar msozeau2008-03-24
* Do a second pass on the treatment of user-given implicit arguments. NowGravatar msozeau2008-03-15
* 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
* Plus de combinateurs sont passés de Util à Option. Le module Options Gravatar aspiwack2007-12-06
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
* Uniformisation politique de nommage evd/isevars (evd si evar_defs,Gravatar herbelin2007-09-06
* - Débogueur: positionnement de set_detype_anonymous pour ne pasGravatar herbelin2007-08-29
* Slight cleanup of refl_omega.ml : in particular it uses now listGravatar letouzey2007-07-11
* Fix bug in subst_cases_pattern when aliasing recursive notations.Gravatar msozeau2007-07-02
* Nouveaux changements autour des implicites (notamment suite àGravatar herbelin2007-05-06
* Multiples changements autour des implicites :Gravatar herbelin2007-04-29
* Correction bug #1477 sur ordre des variables partagées par les or-patterns.Gravatar herbelin2007-04-13
* 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
* Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé deGravatar herbelin2007-02-13
* Correction bug #1364 (les variables de section sont repérées parGravatar herbelin2007-02-07
* 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
* Tentative d'amélioration du message d'erreur en cas de paramètre non laisséGravatar herbelin2006-09-24
* Correction bug dans détection clause "in" mal formée quand le "in" estGravatar herbelin2006-09-24
* Declarative Proof Language: main commitGravatar corbinea2006-09-20
* Export de fonctions d'interprétation acceptant des evars non résoluesGravatar herbelin2006-09-01
* 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
* Réinitialisation de token_number à chaque compilation d'un nouveau fichier ...Gravatar notin2006-06-08
* Adaptation de Coqdoc au nouveau add_globGravatar notin2006-05-24
* Retour version 8852 de constrintern.mlGravatar herbelin2006-05-23
* Erreur commit constrintern.mlGravatar herbelin2006-05-23
* Changement de précédence de l'argument du by de assert; conséquences...Gravatar herbelin2006-05-23
* Modification de add_glob (support des modules dans Coqdoc)Gravatar notin2006-05-23
* r8931@thot: notin | 2006-04-28 16:19:38 +0200Gravatar notin2006-04-28
* Typo dans précédent commit (8755); protection renforcée dans analyse claus...Gravatar herbelin2006-04-28
* - Distinction explicite des parties paramètres et arguments dans le typeGravatar herbelin2006-04-27
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
* préparation de add_glob en vue d'isolement de la partie module pourGravatar herbelin2006-04-27
* Si un fixpoint a plusieurs arguments, mais un seul de type inductif, Gravatar letouzey2006-04-14
* Made pretyping a functor over a coercion implementation. Pretyping.Default us...Gravatar msozeau2006-03-22
* Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.Gravatar msozeau2006-03-13
* Correction message d'erreur ltac et adoption du modèle de message de TacinterpGravatar herbelin2006-03-04