aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
* Rien d'importantGravatar herbelin2003-05-13
* Affichage des Fix contenant des Let dans leur context (ce que la tactique Fix...Gravatar herbelin2003-04-27
* simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...Gravatar letouzey2003-04-16
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07
* Correction bug #261 + amélioration nommageGravatar herbelin2003-04-01
* Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)Gravatar herbelin2003-03-29
* *** empty log message ***Gravatar barras2003-03-21
* *** empty log message ***Gravatar barras2003-03-12
* Bug affichage let destructurantGravatar herbelin2003-02-02
* Backtrack sur le filtrage des applications partielles (change Tauto/Intuition)Gravatar herbelin2003-02-01
* Ajout d'un filtrage d'application partielleGravatar herbelin2003-01-31
* Unification plus efficace vis à vis du LetInGravatar herbelin2003-01-31
* reparation des contribs: lors de l'unification, reduire les beta redexesGravatar barras2003-01-23
* modified the unification algorithm to try first order unification beforeGravatar barras2003-01-22
* ajout de whd_state dans l'interfaceGravatar barras2003-01-22
* LocalisationGravatar herbelin2003-01-19
* Problème de désynchronisation des variables du type et du corps d'un point-...Gravatar herbelin2003-01-15
* Bug en présence de let-inGravatar herbelin2003-01-15
* Prise en compte application partielle dans dependentGravatar herbelin2002-12-23
* Légère amélioration des messages d'erreur des with-bindings et des RewriteGravatar herbelin2002-12-21
* Affinement affichageGravatar herbelin2002-12-21
* Petit netoyage dans libGravatar coq2002-12-19
* apres correction du probleme de Global.env, retour du mis_constr_nargs_envGravatar letouzey2002-12-19
* ma bidouille marche pas...Gravatar letouzey2002-12-17
* correction (temporaire ?) d'un probleme de Printer.prterm_env utilisant quand...Gravatar letouzey2002-12-13
* CommentairesGravatar herbelin2002-12-10
* Essai suppression nf_betaiota dans type_ofGravatar herbelin2002-12-09
* Problèmes et améliorations divers affichageGravatar herbelin2002-12-09
* Ajout Simpl et Change sur des sous-termesGravatar herbelin2002-12-09
* Allègement du noyauGravatar herbelin2002-11-18
* Ajout de Cases dans abbreviatable constr (aconstr) [utilisé dans laGravatar herbelin2002-11-18
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Un revenant hors sujetGravatar herbelin2002-11-13
* Intégration des modifs de la branche mowgli :Gravatar herbelin2002-11-05
* Moins de restriction sur le commit 1.5Gravatar herbelin2002-10-17
* nom de fonction plus simpleGravatar barras2002-10-15
* Moins de restriction sur le commit précédentGravatar herbelin2002-10-13
* Ajout map_rawconstrGravatar herbelin2002-10-13
* Restriction sur la forme des Syntactic Definition et re-localisation en fonct...Gravatar herbelin2002-10-12
* retour en arriere concernant la recherche d'occurence modulo expansion des le...Gravatar barras2002-10-09
* Vraie substitutivite de autohintsGravatar coq2002-10-01
* Un peu (plus) d'ordre dans Nametab...Gravatar coq2002-09-24
* Amélioration messages d'erreur non inférence implicitesGravatar herbelin2002-09-03
* pretyping/pretyping.mlGravatar herbelin2002-09-03
* correction de bugs:Gravatar barras2002-08-16
* Renoncement à distinguer les types "constr" et "types"; nettoyageGravatar herbelin2002-08-13
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* un cas inutile dans un pattern matchingGravatar letouzey2002-07-16