aboutsummaryrefslogtreecommitdiff
path: root/library
AgeCommit message (Expand)Author
2016-03-04Fix #4607: do not read native code files if native compiler was disabled.Maxime Dénès
2016-02-03Optimizing the universes_of_constr_function.Pierre-Marie Pédrot
2016-01-23Fix bug #4503: mixing universe polymorphic and monomorphicMatthieu Sozeau
2016-01-20Update copyright headers.Maxime Dénès
2016-01-15Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.Maxime Dénès
2016-01-06Protect code against changes in Map interface.Maxime Dénès
2015-12-03Univs: fix bug #4443.Matthieu Sozeau
2015-11-27Univs: entirely disallow instantiation of polymorphic constants withMatthieu Sozeau
2015-11-27Avoid recording spurious Set <= Top.i constraints which are alwaysMatthieu Sozeau
2015-11-20Univs: fix type_of_global_in_context not returning instantiated universe cont...Matthieu Sozeau
2015-10-30Add a way to get the right fix_exn in external vernacular commandsMatthieu Sozeau
2015-10-28Univs: local names handling.Matthieu Sozeau
2015-10-28Avoid type checking private_constants (side_eff) again during Qed (#4357).Enrico Tassi
2015-10-28lib_stack: API to reorder the libstackEnrico Tassi
2015-10-27Fix bugs 4389, 4390 and 4391 due to wrong handling of universe namesMatthieu Sozeau
2015-10-25Declaremods: replace two anomalies by user errors (fix #3974 and #3975)Pierre Letouzey
2015-10-13Fix some typos.Guillaume Melquiond
2015-10-08Univs: fix bug #3807Matthieu Sozeau
2015-10-08Goptions: new value type: optional stringEnrico Tassi
2015-10-02Univs: Change intf of push_named_def to return the computed universeMatthieu Sozeau
2015-10-02Univs: refined handling of assumptionsMatthieu Sozeau
2015-10-02Univs: fix minimization to allow lowering a universe to Set, not Prop.Matthieu Sozeau
2015-10-02Univs: fix Universe vernacular, fix bug #4287.Matthieu Sozeau
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-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-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-24On-demand Require.Pierre-Marie Pédrot
2015-06-24Splitting the library representation on disk in two.Pierre-Marie Pédrot
2015-06-11Fix bug #3446.Matthieu Sozeau
2015-05-27Fix bug #4159Matthieu Sozeau
2015-05-14Disable precompilation for native_compute by default.Guillaume Melquiond
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 18:38:36 +0000