aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/reserve.ml
Commit message (Expand)AuthorAge
...
* Death of "survive_module" and "survive_section" (the first one wasGravatar herbelin2009-08-13
* Move Record desugaring to constrintern and add ability to use notationsGravatar msozeau2008-11-05
* Open notation for declaring record instances.Gravatar msozeau2008-10-23
* - Second pass on implementation of let pattern. Parse "let ' par [as x]?Gravatar msozeau2008-03-28
* Add new LetPattern construct to replace dest. syntax: let| pat := t in b is b...Gravatar msozeau2008-01-17
* 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
* Add a parameter to QuestionMark evar kind to say it can be turned into an obl...Gravatar msozeau2007-03-19
* Pas d'escamotage des noms réservés si Set Printing All actibvéGravatar herbelin2006-12-08
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Changement des named_contextGravatar gregoire2005-12-02
* hiding the meta_map in evar_defsGravatar barras2004-09-15
* Nouvelle en-têteGravatar herbelin2004-07-16
* modif des fixpoints pour que si on donne une notation au produit, les pts fix...Gravatar barras2004-03-05
* meilleure presentation des commentaires du traducteurGravatar barras2004-01-02
* Substitution dans REvar et PEvar plutot que encodage via noeud application po...Gravatar herbelin2003-12-19
* Correction du bug 335 et Export/Require Export dans un moduleGravatar coq2003-10-07
* Renommage des variables '_'Gravatar herbelin2003-09-10
* Ajout construction If primitive dans constr_expr et rawconstrGravatar herbelin2003-09-09
* Ajout LetTupleGravatar herbelin2003-08-11
* Nouvelle mouture du traducteur v7->v8Gravatar herbelin2003-08-11
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
* Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)Gravatar herbelin2003-03-29