aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Export type_of_global_ref (useful for external users of glob files)Gravatar Enrico Tassi2014-07-11
* make the standard logging facility stm awareGravatar Enrico Tassi2014-07-11
* MSetRBT: unfortunate typo in compare_height (fix #3413)Gravatar Pierre Letouzey2014-07-10
* Better handling of the universe context in case of Admitted proof obligations.Gravatar Matthieu Sozeau2014-07-10
* Overlooked to remove a change in kernel/closure that made reducing underGravatar Matthieu Sozeau2014-07-10
* option to always delegate futures to workersGravatar Enrico Tassi2014-07-10
* CoqIDE: on win32 the old interrputer code (SIGINT) is still neededGravatar Enrico Tassi2014-07-10
* more APIs in TQueue and CThreadGravatar Enrico Tassi2014-07-10
* check_for_interrupt: better (but slower) in threading modeGravatar Enrico Tassi2014-07-10
* Reduce non-toplevel letins in splay_prod_assum (bug found in Ergo).Gravatar Matthieu Sozeau2014-07-10
* Fix a oversight in 5bf9e67b .Gravatar Arnaud Spiwack2014-07-10
* Revert patch making the oracle be used for the transparent state in evarconv,Gravatar Matthieu Sozeau2014-07-09
* Locate: also display some information about module aliasingGravatar Pierre Letouzey2014-07-09
* Arith: full integration of the "Numbers" modular frameworkGravatar Pierre Letouzey2014-07-09
* Fixing the previous patch to keep transparent states in sync.Gravatar Pierre-Marie Pédrot2014-07-09
* Recovering transparent state from kernel oracles in constant time.Gravatar Pierre-Marie Pédrot2014-07-09
* Fixing bug #3270. Patch by Robbert Krebbers.Gravatar Pierre-Marie Pédrot2014-07-08
* Exporting Proof.split in proofview.Gravatar Pierre-Marie Pédrot2014-07-08
* Revert "time tac" (committed by mistake).Gravatar Hugo Herbelin2014-07-07
* time tacGravatar Hugo Herbelin2014-07-07
* Updating README wrt coq-club and ftp.Gravatar Hugo Herbelin2014-07-07
* Fix g_coqast for explicit applications.Gravatar Matthieu Sozeau2014-07-07
* Coq_makefile: fix cmx compilation when there are both ml and mllibGravatar Pierre Boutillier2014-07-07
* In flex-flex cases, the undefinedness of an evar can not be preseved after co...Gravatar Matthieu Sozeau2014-07-07
* Missing check of evar instantiation, resulting in missing constraints (bug fr...Gravatar Matthieu Sozeau2014-07-07
* In dest_prod_assum, allow non-toplevel let-reductions (fixes a bug found in M...Gravatar Matthieu Sozeau2014-07-07
* Using IStream coiterator to explicit the captured state of tactic matching re...Gravatar Pierre-Marie Pédrot2014-07-05
* Cleanup code related to the constraint solving, which sits now outside theGravatar Matthieu Sozeau2014-07-03
* Properly compute the transitive closure of the system of constraintsGravatar Matthieu Sozeau2014-07-03
* Restore proper order of effects in letin_tac_gen. Fixes CFGV again.Gravatar Matthieu Sozeau2014-07-03
* Fix eta expansion of primitive records (HoTT bug #78), which now fails cleanl...Gravatar Matthieu Sozeau2014-07-03
* Fix Coq_makefile in presence of mlpackGravatar Pierre Boutillier2014-07-03
* coqdoc is minimaly -Q awareGravatar Pierre Boutillier2014-07-03
* Adding a coiterator to IStream.Gravatar Pierre-Marie Pédrot2014-07-03
* More efficient implementation of Ltac match, by inlining a stream map.Gravatar Pierre-Marie Pédrot2014-07-03
* When defining a monomorphic Program, do not allow arbitrary instantiationsGravatar Matthieu Sozeau2014-07-03
* Bug 3405: Coq_makefile: Implicit rules only for listed files in Make fileGravatar Pierre Boutillier2014-07-03
* In setoid_rewrite, force resolution of the contraints generated by rewriting ...Gravatar Matthieu Sozeau2014-07-02
* Fix a Not_found anomaly raised by solve_evar_evar, we were breaking theGravatar Matthieu Sozeau2014-07-02
* Indeed simpl never is really honored now.Gravatar Matthieu Sozeau2014-07-02
* Add toplevel commands to declare global universes and constraints.Gravatar Matthieu Sozeau2014-07-01
* Patch from Enrico Tassi to get Drop compatible with stm.Gravatar Enrico Tassi2014-07-01
* Continuing ff9f94634 on making code and doc agree on "Set Equality Schemes"Gravatar Hugo Herbelin2014-07-01
* Making code and doc agree on "Set Equality Schemes" (see also bug #2550).Gravatar Hugo Herbelin2014-07-01
* Fixing the place where to insert a space in "Tactic failure"Gravatar Hugo Herbelin2014-07-01
* More informative message when Mltop.load_object fails.Gravatar Hugo Herbelin2014-07-01
* Useless keeping of dirpath in tactic aliases.Gravatar Pierre-Marie Pédrot2014-06-30
* Clarifying 'No such bound variable' message in apply, as suggested in #2387Gravatar Hugo Herbelin2014-06-30
* Tests for bugs #2834 and #2994.Gravatar Hugo Herbelin2014-06-30
* Completing test for bug report #2830Gravatar Hugo Herbelin2014-06-30
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 09:20:21 +0000