aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
Commit message (Expand)AuthorAge
* Univs: fix bug #4443.Gravatar Matthieu Sozeau2015-12-03
* Univs: entirely disallow instantiation of polymorphic constants withGravatar Matthieu Sozeau2015-11-27
* Avoid recording spurious Set <= Top.i constraints which are alwaysGravatar Matthieu Sozeau2015-11-27
* Univs: fix type_of_global_in_context not returning instantiated universe cont...Gravatar Matthieu Sozeau2015-11-20
* Add a way to get the right fix_exn in external vernacular commandsGravatar Matthieu Sozeau2015-10-30
* Univs: local names handling.Gravatar Matthieu Sozeau2015-10-28
* Avoid type checking private_constants (side_eff) again during Qed (#4357).Gravatar Enrico Tassi2015-10-28
* lib_stack: API to reorder the libstackGravatar Enrico Tassi2015-10-28
* Fix bugs 4389, 4390 and 4391 due to wrong handling of universe namesGravatar Matthieu Sozeau2015-10-27
* Declaremods: replace two anomalies by user errors (fix #3974 and #3975)Gravatar Pierre Letouzey2015-10-25
* Fix some typos.Gravatar Guillaume Melquiond2015-10-13
* Univs: fix bug #3807Gravatar Matthieu Sozeau2015-10-08
* Goptions: new value type: optional stringGravatar Enrico Tassi2015-10-08
* Univs: Change intf of push_named_def to return the computed universeGravatar Matthieu Sozeau2015-10-02
* Univs: refined handling of assumptionsGravatar Matthieu Sozeau2015-10-02
* Univs: fix minimization to allow lowering a universe to Set, not Prop.Gravatar Matthieu Sozeau2015-10-02
* Univs: fix Universe vernacular, fix bug #4287.Gravatar Matthieu Sozeau2015-10-02
* Univs: minimization, adapt to graph invariants.Gravatar Matthieu Sozeau2015-10-02
* Forcing i > Set for global universes (incomplete)Gravatar Matthieu Sozeau2015-10-02
* Universes: enforce Set <= i for all Type occurrences.Gravatar Matthieu Sozeau2015-10-02
* Unexport Loadpath.get_paths.Gravatar Guillaume Melquiond2015-09-30
* Fix dumb typo.Gravatar Guillaume Melquiond2015-09-29
* Make the interface of System.raw_extern_intern much saner.Gravatar Guillaume Melquiond2015-09-29
* Prevent States.intern_state and System.extern_intern from looking up files in...Gravatar Guillaume Melquiond2015-09-29
* Remove some uses of Loadpath.get_paths.Gravatar Guillaume Melquiond2015-09-29
* Make -load-vernac-object respect the loadpath.Gravatar Guillaume Melquiond2015-09-28
* The -require option now accepts a logical path instead of a physical one.Gravatar Pierre-Marie Pédrot2015-09-25
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 17:15:01 +0000