aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* update md5 sums to make "make check" workGravatar Enrico Tassi2014-12-19
|
* Fix sigsegv in checkerGravatar Enrico Tassi2014-12-19
|
* Better doc and a few fixes for Proof using.Gravatar Enrico Tassi2014-12-19
|
* Back to the preferred ?n1:=?n2 order of evar-evar unification which got ↵Gravatar Hugo Herbelin2014-12-19
| | | | accidentally mixed up in 9aa416c0c6.
* Fixing wrong notation level in #3295.Gravatar Hugo Herbelin2014-12-19
|
* Adds two lemmas about hderror to the List standard library.Gravatar Sébastien Hinderer2014-12-18
|
* Implement the nodup function on lists and prove associated results.Gravatar Sébastien Hinderer2014-12-18
|
* Lists: enhanced version of Seb's last commit on Exists/ForallGravatar Pierre Letouzey2014-12-18
|
* Lists: a few results on Exists and Forall and a bit of code cleanup.Gravatar Sébastien Hinderer2014-12-18
|
* Fixing checker representation of universe lists.Gravatar Pierre-Marie Pédrot2014-12-18
|
* Backporting the change in lists of universes to the checker.Gravatar Pierre-Marie Pédrot2014-12-18
|
* Cleaning up universe list implementation in Univ.Gravatar Pierre-Marie Pédrot2014-12-18
| | | | | | We use private types to ensure apriori hashconsing, and get rid of the use of recursive modules. The hash of the universe list is also inlined into each node instead of relying on a supplementary indirection.
* Proof using: New vernacular to name sets of section variablesGravatar Enrico Tassi2014-12-18
|
* Bug fix (coq_makefile): Adding unix.cma and threads.cma dependencies for ↵Gravatar mlasson2014-12-18
| | | | grammar in campl4
* Fixed bad newlines in output for std output and emacs.Gravatar Pierre Courtieu2014-12-18
| | | | | I added a emacs_logger. Still need to cleanup std_logger.
* Fix compilation with ocaml 4.0.0Gravatar Enrico Tassi2014-12-17
|
* checker: Change in library on disk values, now using context_sets instead ofGravatar Matthieu Sozeau2014-12-17
| | | | constraints only.
* Ensuring the good invariants of hashcons table generation in the API.Gravatar Pierre-Marie Pédrot2014-12-17
|
* Fix (actually, properly implement :) hashconsing of projections,Gravatar Matthieu Sozeau2014-12-17
| | | | | resulting in huge speedup at Qed/section closing in presence of primitive projections.
* Fixing bug #3796.Gravatar Pierre-Marie Pédrot2014-12-17
|
* Fixing Makefile so that it puts the -thread flag on the right place.Gravatar Pierre-Marie Pédrot2014-12-17
|
* Update checker/values and cic due to changes in case_info and record_body.Gravatar Matthieu Sozeau2014-12-17
|
* Future: blocking by defaultGravatar Enrico Tassi2014-12-17
| | | | | | This makes queries like Print or Extraction block and not raise the error "the value is not ready". This should make CoqIDE work for every kind of script.
* STM: resilient on errors in non delegated proofsGravatar Enrico Tassi2014-12-17
| | | | | | | | | | | | | | This commits makes the concept of delegated and async more orthogonal. A proof can be async but not delegated to a worker (if it is known to be very small it is too much overhead to delegate to a worker). A proof that is not async cannot be delegated to a worker. An async proof that contains an error does not prevent Coq from continuing the execution (interactive mode) and can be fixed without invalidating the whole document (CoqIDE knows how to do that) even if it is processed locally. It used to be the case only for delegated proofs, now it worker for all the proofs that can be in principle delegated (doing it or not is an implementation detail, an optimization).
* CoqIDE: cleanup jobs window on worker deathGravatar Enrico Tassi2014-12-17
|
* STM: rename and simplify flagsGravatar Enrico Tassi2014-12-17
|
* STM: simplify state managementGravatar Enrico Tassi2014-12-17
| | | | | | | Thanks the the previous patchset a worker can be asked to send back "light" version of the system states. This is reasonably efficient hence the idea of letting a worker hang around just to hold system states for retrieval on demand is dropped.
* AsyncTaskQueue: simpler model (no parking area, continuation tasks)Gravatar Enrico Tassi2014-12-17
|
* WorkerPool: simpler fuctor and no more parking areaGravatar Enrico Tassi2014-12-17
|
* TQueue: a way to unblock threads begin destroyed waiting on popGravatar Enrico Tassi2014-12-17
|
* Spawn: fix request of Gc statisticsGravatar Enrico Tassi2014-12-17
|
* CThread: use a different type for thread friendly in_channelsGravatar Enrico Tassi2014-12-17
|
* Summary: more surgery functionsGravatar Enrico Tassi2014-12-17
| | | | | API to let one forge a frozen state out of another frozen state plus some frozen bits
* Global: export the name of the summary entryGravatar Enrico Tassi2014-12-17
| | | | | | In this way one can make surgery on the system states, like checking if two frozen states have the same environment (i.e. no running "abstract" in between)
* Dyn: add API to check of two Dyn.t are ==Gravatar Enrico Tassi2014-12-17
| | | | | A Dyn.t boxes a type tag with the original object, so calling == on the Dyn.t does not work, hence this extra API.
* Arguments: warn only if no option is given (Close 3860)Gravatar Enrico Tassi2014-12-17
|
* CoqIDE: better messagesGravatar Enrico Tassi2014-12-17
|
* Revert and correctly fix "#4843 part 2 : The .cmxs files for plugins must ↵Gravatar Pierre Boutillier2014-12-17
| | | | | | have x permission" This reverts commit 607503b28fca50f4b76b2237d5ca13802b8252fa.
* #3828 is solved.Gravatar Hugo Herbelin2014-12-16
|
* Moving #2447 (congruence) to fixed.Gravatar Hugo Herbelin2014-12-16
|
* In CHANGES, alerting about stronger check on notation level modifiers.Gravatar Hugo Herbelin2014-12-16
|
* More printers for ltac signatures.Gravatar Hugo Herbelin2014-12-16
|
* Test for #3654.Gravatar Hugo Herbelin2014-12-16
|
* fix bug #2447 in congruenceGravatar Pierre Corbineau2014-12-16
|\
* | fix bug #2447 in congruenceGravatar Pierre Corbineau2014-12-16
| |
| * Fixing CAMLP4 compilation.Gravatar Pierre-Marie Pédrot2014-12-16
| |
| * msg_info now puts infomsg tag in emacs mode.Gravatar Pierre Courtieu2014-12-16
| | | | | | | | | | Fixes the idtac "string" not appearing in proofgeneral because printined *before* the goal.
| * Proper thread-safe implementation for Exninfo.Gravatar Pierre-Marie Pédrot2014-12-16
| | | | | | | | | | This is the second part of the Exninfo patch. It introduces dependency in the Thread library in all Coq files.
| * Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Instead of modifying exceptions to wear additional information, we instead use a dedicated type now. All exception-using functions were modified to support this new type, in particular Future's fix_exn-s and the tactic monad. To solve the problem of enriching exceptions at raise time and recover this data in the try-with handler, we use a global datastructure recording the given piece of data imperatively that we retrieve in the try-with handler. We ensure that such instrumented try-with destroy the data so that there may not be confusion with another exception. To further harden the correction of this structure, we also check for pointer equality with the last raised exception. The global data structure is not thread-safe for now, which is incorrect as the STM uses threads and enriched exceptions. Yet, we splitted the patch in two parts, so that we do not introduce dependencies to the Thread library immediatly. This will allow to revert only the second patch if ever we switch to OCaml-coded lightweight threads.
| * Error messages of Searchxxx are coherent with goal selector.Gravatar Pierre Courtieu2014-12-16
|/ | | | | | If a goal is given and wrong, exception is raised. If no goal is given, then goal 1 is tried but no failure if goal 1 does not exist, just fall back to gloab env.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 22:13:36 +0000