aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/coercion.mli
Commit message (Expand)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\
| * Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
* | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
|/
* Making judgment type generic over the type of inner constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Coercion API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* A few Global.env removed.Gravatar Hugo Herbelin2014-10-04
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* TC: honor the use_typeclasses flag in pretypingGravatar Enrico Tassi2014-02-12
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* Updating headers.Gravatar herbelin2012-08-08
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* remove many excessive open Util & Errors in mli'sGravatar letouzey2012-05-29
* Second step of integration of Program:Gravatar msozeau2012-03-14
* Remove support for "abstract typing constraints" that requires unicity of sol...Gravatar msozeau2012-03-14
* Noise for nothingGravatar pboutill2012-03-02
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Promote evar_defs to evar_map (in Evd)Gravatar glondu2009-11-11
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Various improvements in handling of evars in general and typingGravatar msozeau2008-06-21
* Prise en compte des coercions dans les clauses "with" même si le typeGravatar herbelin2008-04-23
* The "clean integration of subtac" patch.Gravatar msozeau2006-05-29
* - Documentation of the Program tactics.Gravatar msozeau2006-04-07
* Made pretyping a functor over a coercion implementation. Pretyping.Default us...Gravatar msozeau2006-03-22
* Localisation des erreurs de sorte du prétypageGravatar herbelin2006-02-08
* DocumentationGravatar herbelin2006-01-29
* deuxieme vague de modifs: evar_defs fonctionnelGravatar barras2004-09-07
* Nouvelle en-têteGravatar herbelin2004-07-16
* Suppression de Rawterm.loc, branchement sur Util.locGravatar herbelin2004-07-16
* Mise en place de coercion dans les motifsGravatar herbelin2001-12-11
* Suppression des local_constraints, des ctxtty et du focus.Gravatar clrenard2001-11-06
* L'instantiation des evars quand un produit ou une sorte étaient attendus n'Ã...Gravatar herbelin2001-09-14
* entetesGravatar filliatr2001-03-15
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* Insertion de coercion au milieu des applications partielles et propagation de...Gravatar herbelin2000-11-08
* Nettoyage CoercionGravatar herbelin2000-10-19
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Séparation des contraintes de type et de valeur dans pretypingGravatar herbelin2000-06-29
* Bugs et simplifications coercionsGravatar herbelin2000-06-02
* Mise en place d'un choix constr/typed_type en remplacement de certains CastGravatar herbelin2000-06-01
* Afficahge des locationsGravatar herbelin2000-05-31
* Export inh_conv_coerce_to et diversGravatar herbelin2000-03-07
* gros commit de tout ce que j'ai fait pendant les vacances :Gravatar filliatr2000-01-21
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-06 10:42:03 +0000