aboutsummaryrefslogtreecommitdiff
path: root/library
AgeCommit message (Expand)Author
2015-10-02Univs: minimization, adapt to graph invariants.Matthieu Sozeau
2015-10-02Forcing i > Set for global universes (incomplete)Matthieu Sozeau
2015-10-02Universes: enforce Set <= i for all Type occurrences.Matthieu Sozeau
2015-09-30Unexport Loadpath.get_paths.Guillaume Melquiond
2015-09-29Fix dumb typo.Guillaume Melquiond
2015-09-29Make the interface of System.raw_extern_intern much saner.Guillaume Melquiond
2015-09-29Prevent States.intern_state and System.extern_intern from looking up files in...Guillaume Melquiond
2015-09-29Remove some uses of Loadpath.get_paths.Guillaume Melquiond
2015-09-28Make -load-vernac-object respect the loadpath.Guillaume Melquiond
2015-09-25Show assumptions of well-foundedness in `Print Assumptions`Arnaud Spiwack
2015-09-25The -require option now accepts a logical path instead of a physical one.Pierre-Marie Pédrot
2015-09-25The -compile option now accepts ".v" files and outputs a warning otherwise.Pierre-Marie Pédrot
2015-09-25Propagate `Guarded` flag from syntax to kernel.Arnaud Spiwack
2015-09-23Hopefully better names to constructors of internal_flag, as discussedHugo Herbelin
2015-09-20Nametab: print debug notice only in debug mode.Maxime Dénès
2015-09-03Add an if_verbose for "Fetching opaque proofs ..."mlasson
2015-07-16Fixing anomaly #3743 while printing an error message involving evar constraints.Hugo Herbelin
2015-07-10Option -type-in-type: added support in checker and making it contaminatingHugo Herbelin
2015-07-10Native compiler: refactor code handling pre-computed values.Maxime Dénès
2015-07-09Improve semantics of -native-compiler flag.Maxime Dénès
2015-07-07Univs/minimization: Fix unused variable bug.Matthieu Sozeau
2015-06-29Assumptions: more informative print for False axiom (Close: #4054)Enrico Tassi
2015-06-26Fix bug #4254 with the help of J.H. JourdanMatthieu Sozeau
2015-06-25Wrapped the declare_object function to pretty-print anomalies at loading time.Thomas Sibut-Pinote
2015-06-24Make inductives that were assumed positive appear in `Print Assumptions`.Arnaud Spiwack
2015-06-24Add a corresponding field in `mutual_inductive_entry` (part 1).Arnaud Spiwack
2015-06-24Merge branch 'v8.5'Pierre-Marie Pédrot
2015-06-24On-demand Require.Pierre-Marie Pédrot
2015-06-24Splitting the library representation on disk in two.Pierre-Marie Pédrot
2015-06-23Wrapped the declare_object function to pretty-print anomalies at loading time.Thomas Sibut-Pinote
2015-06-11Fix bug #3446.Matthieu Sozeau
2015-05-27Fix bug #4159Matthieu Sozeau
2015-05-14Disable precompilation for native_compute by default.Guillaume Melquiond
2015-04-23Remove almost all the uses of string concatenation when building error messages.Guillaume Melquiond
2015-04-22Tactical `progress` compares term up to potentially equalisable universes.Arnaud Spiwack
2015-04-17Extra fix to 934761875 and f4ee7ee31e4 on optimizing Import of severalHugo Herbelin
2015-04-09Strengthen minimization: it shouldn't set a universe u to a max if itMatthieu Sozeau
2015-04-02Make it possible for -R to override the existing implicit setting of a path.Guillaume Melquiond
2015-04-01From X Require Y looks for X with absolute path, disregarding -R.Pierre-Marie Pédrot
2015-04-01Removing a probably incorrect on-the-fly require in a tactic.Pierre-Marie Pédrot
2015-03-31Removing the unused root flag from loadpaths.Pierre-Marie Pédrot
2015-03-31A more reasonable implementation of Loadpath.Pierre-Marie Pédrot
2015-03-25Summary: fix code to detect functional values in summaryEnrico Tassi
2015-03-23Dedicated type for on-demand objects in Library.Pierre-Marie Pédrot
2015-03-16Removing the whole library content from the summary.Pierre-Marie Pédrot
2015-03-16More invariants in Library.Pierre-Marie Pédrot
2015-03-11admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Enrico Tassi
2015-02-25STM: proof state also includes meta countersEnrico Tassi
2015-02-24Refactoring in [Constr].Arnaud Spiwack
2015-02-23Fix some typos in comments.Guillaume Melquiond
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 05:26:33 +0000