aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/program.ml
Commit message (Expand)AuthorAge
* Removing some return type compatibility layers in Termops.Gravatar Pierre-Marie Pédrot2017-02-14
* Cases API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Coercion API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-08
|\
| * Fix bug #5066: Anomaly: cannot find Coq.Logic.JMeq.JMeq.Gravatar Pierre-Marie Pédrot2016-10-08
|/
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Program: cleanup in cases, add optionsGravatar Matthieu Sozeau2016-06-29
* Rework treatment of default transparency of obligationsGravatar Matthieu Sozeau2016-06-27
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* Correct rebase on STM code. Thanks to E. Tassi for help on dealing withGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* invalid_arg instead of raise (Invalid_argement ...)Gravatar letouzey2013-03-12
* Dir_path --> DirPathGravatar letouzey2013-02-19
* Minor code cleanups, especially take advantage of Dir_path.is_emptyGravatar letouzey2013-02-18
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Modulification of identifierGravatar ppedrot2012-12-14
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* Everything compiles again.Gravatar msozeau2012-03-14
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 06:08:25 +0000