aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/reserve.ml
Commit message (Expand)AuthorAge
* 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