aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
Commit message (Expand)AuthorAge
* The -compile option now accepts ".v" files and outputs a warning otherwise.Gravatar Pierre-Marie Pédrot2015-09-25
* Hopefully better names to constructors of internal_flag, as discussedGravatar Hugo Herbelin2015-09-23
* Nametab: print debug notice only in debug mode.Gravatar Maxime Dénès2015-09-20
* Add an if_verbose for "Fetching opaque proofs ..."Gravatar mlasson2015-09-03
* Fixing anomaly #3743 while printing an error message involving evar constraints.Gravatar Hugo Herbelin2015-07-16
* Option -type-in-type: added support in checker and making it contaminatingGravatar Hugo Herbelin2015-07-10
* Native compiler: refactor code handling pre-computed values.Gravatar Maxime Dénès2015-07-10
* Improve semantics of -native-compiler flag.Gravatar Maxime Dénès2015-07-09
* Univs/minimization: Fix unused variable bug.Gravatar Matthieu Sozeau2015-07-07
* Assumptions: more informative print for False axiom (Close: #4054)Gravatar Enrico Tassi2015-06-29
* Fix bug #4254 with the help of J.H. JourdanGravatar Matthieu Sozeau2015-06-26
* Wrapped the declare_object function to pretty-print anomalies at loading time.Gravatar Thomas Sibut-Pinote2015-06-25
* On-demand Require.Gravatar Pierre-Marie Pédrot2015-06-24
* Splitting the library representation on disk in two.Gravatar Pierre-Marie Pédrot2015-06-24
* Fix bug #3446.Gravatar Matthieu Sozeau2015-06-11
* Fix bug #4159Gravatar Matthieu Sozeau2015-05-27
* Disable precompilation for native_compute by default.Gravatar Guillaume Melquiond2015-05-14
* Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
* Tactical `progress` compares term up to potentially equalisable universes.Gravatar Arnaud Spiwack2015-04-22
* Extra fix to 934761875 and f4ee7ee31e4 on optimizing Import of severalGravatar Hugo Herbelin2015-04-17
* Strengthen minimization: it shouldn't set a universe u to a max if itGravatar Matthieu Sozeau2015-04-09
* Make it possible for -R to override the existing implicit setting of a path.Gravatar Guillaume Melquiond2015-04-02
* From X Require Y looks for X with absolute path, disregarding -R.Gravatar Pierre-Marie Pédrot2015-04-01
* Removing a probably incorrect on-the-fly require in a tactic.Gravatar Pierre-Marie Pédrot2015-04-01
* Removing the unused root flag from loadpaths.Gravatar Pierre-Marie Pédrot2015-03-31
* A more reasonable implementation of Loadpath.Gravatar Pierre-Marie Pédrot2015-03-31
* Summary: fix code to detect functional values in summaryGravatar Enrico Tassi2015-03-25
* Dedicated type for on-demand objects in Library.Gravatar Pierre-Marie Pédrot2015-03-23
* Removing the whole library content from the summary.Gravatar Pierre-Marie Pédrot2015-03-16
* More invariants in Library.Gravatar Pierre-Marie Pédrot2015-03-16
* admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Gravatar Enrico Tassi2015-03-11
* STM: proof state also includes meta countersGravatar Enrico Tassi2015-02-25
* Refactoring in [Constr].Gravatar Arnaud Spiwack2015-02-24
* Fix some typos in comments.Gravatar Guillaume Melquiond2015-02-23
* Fixing 934761875 about optimizing Import of several libraries at once (thanks...Gravatar Hugo Herbelin2015-02-23
* Documenting the caveat of assumption printing in the mli.Gravatar Pierre-Marie Pédrot2015-02-21
* Tentative fix for bug #4078.Gravatar Pierre-Marie Pédrot2015-02-21
* More resilient implementation of Print Assumptions.Gravatar Pierre-Marie Pédrot2015-02-21
* Deprecated options issue a warning.Gravatar Pierre-Marie Pédrot2015-02-17
* Fixing bug #4053.Gravatar Pierre-Marie Pédrot2015-02-17
* Better comment for [type_of_global_unsafe].Gravatar Matthieu Sozeau2015-02-16
* Comment on the unsafe_ functions in Global.Gravatar Matthieu Sozeau2015-02-16
* Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorGravatar Enrico Tassi2015-02-14
* Windows: open .vo files in binary modeGravatar Enrico Tassi2015-02-05
* Properly set module names in presence of -Q. (Fix for bug #3958)Gravatar Guillaume Melquiond2015-02-05
* Optimized Import/Export the same way as Require Import/Export wasGravatar Hugo Herbelin2015-02-04
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Remove dead code.Gravatar Maxime Dénès2015-01-17
* Univs: proper printing of global and local universe names (onlyGravatar Matthieu Sozeau2015-01-17
* Partially revert "Forbid Require inside interactive modules and module types."Gravatar Maxime Dénès2015-01-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 22:46:03 +0000