aboutsummaryrefslogtreecommitdiff
path: root/pretyping/classops.mli
AgeCommit message (Expand)Author
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-04-10Remove call to global env in pretyping.mlMaxime Dénès
2019-04-10Functionalize env in type classesMaxime Dénès
2019-04-10Move vernac-related part of coercions to vernacMaxime Dénès
2019-03-28Merge PR #9743: Relax the ambiguous path condition of coercionEnrico Tassi
2019-03-25Remove `Automatic Coercions Import` option.Maxime Dénès
2019-03-14Relax the ambiguous path condition of coercionKazuhiko Sakaguchi
2018-09-10Remove environment passing to coercion printersGaëtan Gilbert
2018-09-07Warnings on coercions used without being ImportedMaxime Dénès
2018-07-26Coercions cleanup: use GlobRef.t instead of constrMaxime Dénès
2018-07-24Projections use index representationGaëtan Gilbert
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2017-12-11[proof] Embed evar_map in RefinerError exception.Emilio Jesus Gallego Arias
2017-11-06[api] Deprecate all legacy uses of Names in core.Emilio Jesus Gallego Arias
2017-07-27deprecate Pp.std_ppcmds type aliasMatej Košík
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-04-27Remove unused [open] statementsGaetan Gilbert
2017-04-01Using delayed universe instances in EConstr.Pierre-Marie Pédrot
2017-02-14Making judgment type generic over the type of inner constrs.Pierre-Marie Pédrot
2017-02-14Coercion API using EConstr.Pierre-Marie Pédrot
2017-02-14Classops API using EConstr.Pierre-Marie Pédrot
2016-04-04Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...Matthieu Sozeau
2016-01-20Update copyright headers.Maxime Dénès
2015-08-14Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080Jason Gross
2015-07-10Continuing handling of NoCoercion after df6e64fd28 and 4944b5e72.Hugo Herbelin
2015-01-12Update headers.Maxime Dénès
2014-10-04A few Global.env removed.Hugo Herbelin
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
2014-06-17Adapt coercion code to work with projections as target classes.Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 5)letouzey
2013-03-11Added a Local Definition vernacular command. This type of definitionppedrot
2012-11-25More equality functionsppedrot
2012-08-08Updating headers.herbelin
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2011-02-11An automatic substitution of scope at functor applicationletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-04-29Various minor improvements of comments in mli for ocamldocletouzey
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2008-09-02Propagating commit 11343 from branch v8.2 to trunk (wish 1934 aboutherbelin
2008-04-23Prise en compte des coercions dans les clauses "with" même si le typeherbelin
2005-02-18Moving centralised discharge into dispatched discharge_function; required to ...herbelin
2004-11-16Names.substitution (and related functions) and Term.subst_mps moved tosacerdot
2004-07-16Nouvelle en-têteherbelin
2003-09-12Déplacement de Declare juste à la fin de interp pour pouvoir accéder à in...herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:42:19 +0000