aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrintern.mli
Commit message (Expand)AuthorAge
* Added multiple implicit arguments rules per name.Gravatar herbelin2010-10-03
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Extension of the recursive notations mechanismGravatar herbelin2010-07-22
* Simplified the way internalization_data (i.e. bindings of bound varsGravatar herbelin2010-07-22
* Constrintern: unified push_name_env and push_loc_name_env; madeGravatar herbelin2010-07-22
* Switch to American spelling for "internalise" and "internalisation"Gravatar herbelin2010-07-22
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Various minor improvements of comments in mli for ocamldocGravatar letouzey2010-04-29
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Backport fixes in Instance declarations to Program Instance.Gravatar msozeau2010-01-28
* Promote evar_defs to evar_map (in Evd)Gravatar glondu2009-11-11
* Improving abbreviations/notations + backtrack of semantic change in r12439Gravatar herbelin2009-11-11
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Use more consistent resolution parameters in Program and regular typingGravatar msozeau2009-06-18
* Rewrite of Program Fixpoint to overcome the previous limitations: Gravatar msozeau2009-03-28
* DISCLAIMERGravatar puech2009-01-17
* - Added support for subterm matching in SearchAbout.Gravatar herbelin2008-12-29
* More factorization of inductive/record and typeclasses: move classGravatar msozeau2008-11-09
* Affichage des notations récursives:Gravatar herbelin2008-10-22
* Add enough information to correctly globalize recursive calls in inductive andGravatar msozeau2008-09-11
* Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio...Gravatar notin2008-06-25
* Improvements on coqdoc by adding more information into .globGravatar msozeau2008-05-30
* Postpone the search for the recursive argument index from the user givenGravatar msozeau2008-05-06
* 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
* Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...Gravatar msozeau2007-12-31
* 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
* Support for implicit formal argument types in Program ; parse types in type s...Gravatar msozeau2007-03-28
* Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé deGravatar herbelin2007-02-13
* Declarative Proof Language: main commitGravatar corbinea2006-09-20
* Export de fonctions d'interprétation acceptant des evars non résoluesGravatar herbelin2006-09-01
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Restructuration des points d'entrée de Pretyping et ConstrinternGravatar herbelin2005-12-21
* Conséquences nettoyage pretyping.mlGravatar herbelin2005-09-09
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
* Nouvelle en-têteGravatar herbelin2004-07-16
* pb facto des Fixpoint + erreur avec -dump-glob et LoadGravatar barras2004-04-17
* Gestion maintenant purement fonctionnelle des implicites des point-fixes; ajo...Gravatar herbelin2004-03-27
* Prise en compte des defs syntaxiques dans is_global et global_reference qui p...Gravatar herbelin2003-11-24
* Plus d'uniformite dans la gestion des implicites d'inductifs; nouvelles entre...Gravatar herbelin2003-10-14
* Prise en compte des paramètres implicites d'inductifs pour la globalisation ...Gravatar herbelin2003-10-08
* cosmetiqueGravatar herbelin2003-09-06
* Suppression définitive de lmatch et or_metanum dans tacinterpGravatar herbelin2003-05-21
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
* Mécanisme plus simple et efficace pour traduire les implicitesGravatar herbelin2003-04-09
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 18:36:46 +0000