aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/rawterm.ml
Commit message (Expand)AuthorAge
* Move Record desugaring to constrintern and add ability to use notationsGravatar msozeau2008-11-05
* Open notation for declaring record instances.Gravatar msozeau2008-10-23
* broke cyclic dependenciesGravatar barras2008-07-24
* - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)Gravatar herbelin2008-06-10
* - 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
* 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
* correction d'un bug d'efficacite dans le printerGravatar jforest2007-01-26
* Notations:Gravatar herbelin2006-10-09
* Added {measure x f} as a valid recursion order.Gravatar msozeau2006-06-22
* Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...Gravatar herbelin2006-05-30
* The "clean integration of subtac" patch.Gravatar msozeau2006-05-29
* - Distinction explicite des parties paramètres et arguments dans le typeGravatar herbelin2006-04-27
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
* - Utilisation d'abbréviations pour les types intervenant dans RCasesGravatar herbelin2006-04-26
* 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
* Fonctions de conversion rawconstr <-> cases_patternGravatar herbelin2006-01-08
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Changement des named_contextGravatar gregoire2005-12-02
* HUGE COMMITGravatar sacerdot2005-01-03
* ExtraRedExpr maintenant sans argument: pas très souple mais au moins convien...Gravatar herbelin2004-12-29
* Names.substitution (and related functions) and Term.subst_mps moved toGravatar sacerdot2004-11-16
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* hiding the meta_map in evar_defsGravatar barras2004-09-15
* Correction bug #830 : les noms des implicites temporaires étaient inconnus a...Gravatar herbelin2004-08-23
* Nouvelle en-têteGravatar herbelin2004-07-16
* Suppression de Rawterm.loc, branchement sur Util.locGravatar herbelin2004-07-16
* modif des fixpoints pour que si on donne une notation au produit, les pts fix...Gravatar barras2004-03-05
* - fixed the Assert_failure error in kernel/modopsGravatar barras2004-02-18
* Substitution dans REvar et PEvar plutot que encodage via noeud application po...Gravatar herbelin2003-12-19
* Deplacement subst_rawconstr dans RawtermGravatar herbelin2003-11-19
* Ajout construction If primitive dans constr_expr et rawconstrGravatar herbelin2003-09-09
* Nouvelle mouture du traducteur v7->v8Gravatar herbelin2003-08-11
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07
* Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)Gravatar herbelin2003-03-29
* *** empty log message ***Gravatar barras2003-03-21
* Légère amélioration des messages d'erreur des with-bindings et des RewriteGravatar herbelin2002-12-21
* Ajout Simpl et Change sur des sous-termesGravatar herbelin2002-12-09
* 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
* Ajout map_rawconstrGravatar herbelin2002-10-13
* Restriction sur la forme des Syntactic Definition et re-localisation en fonct...Gravatar herbelin2002-10-12
* pretyping/pretyping.mlGravatar herbelin2002-09-03
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* Finalement un seul constr pour l'instant dans ExtraRedExprGravatar herbelin2002-05-30
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29