aboutsummaryrefslogtreecommitdiff
path: root/pretyping/program.ml
AgeCommit message (Expand)Author
2016-10-08Fix bug #5066: Anomaly: cannot find Coq.Logic.JMeq.JMeq.Pierre-Marie Pédrot
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-29Program: cleanup in cases, add optionsMatthieu Sozeau
2016-06-27Rework treatment of default transparency of obligationsMatthieu Sozeau
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-05-06Correct rebase on STM code. Thanks to E. Tassi for help on dealing withMatthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2013-03-12invalid_arg instead of raise (Invalid_argement ...)letouzey
2013-02-19Dir_path --> DirPathletouzey
2013-02-18Minor code cleanups, especially take advantage of Dir_path.is_emptyletouzey
2013-01-28Uniformization of the "anomaly" command.ppedrot
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-08-08Updating headers.herbelin
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-03-14Everything compiles again.msozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 12:59:25 +0000