| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-12-19 | Back to the preferred ?n1:=?n2 order of evar-evar unification which got ↵ | Hugo Herbelin | |
| accidentally mixed up in 9aa416c0c6. | |||
| 2014-12-19 | Fixing wrong notation level in #3295. | Hugo Herbelin | |
| 2014-12-18 | Adds two lemmas about hderror to the List standard library. | Sébastien Hinderer | |
| 2014-12-18 | Implement the nodup function on lists and prove associated results. | Sébastien Hinderer | |
| 2014-12-18 | Lists: enhanced version of Seb's last commit on Exists/Forall | Pierre Letouzey | |
| 2014-12-18 | Lists: a few results on Exists and Forall and a bit of code cleanup. | Sébastien Hinderer | |
| 2014-12-18 | Fixing checker representation of universe lists. | Pierre-Marie Pédrot | |
| 2014-12-18 | Backporting the change in lists of universes to the checker. | Pierre-Marie Pédrot | |
| 2014-12-18 | Cleaning up universe list implementation in Univ. | Pierre-Marie Pédrot | |
| 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. | |||
| 2014-12-18 | Proof using: New vernacular to name sets of section variables | Enrico Tassi | |
| 2014-12-18 | Bug fix (coq_makefile): Adding unix.cma and threads.cma dependencies for ↵ | mlasson | |
| grammar in campl4 | |||
| 2014-12-18 | Fixed bad newlines in output for std output and emacs. | Pierre Courtieu | |
| I added a emacs_logger. Still need to cleanup std_logger. | |||
| 2014-12-17 | Fix compilation with ocaml 4.0.0 | Enrico Tassi | |
| 2014-12-17 | checker: Change in library on disk values, now using context_sets instead of | Matthieu Sozeau | |
| constraints only. | |||
| 2014-12-17 | Ensuring the good invariants of hashcons table generation in the API. | Pierre-Marie Pédrot | |
| 2014-12-17 | Fix (actually, properly implement :) hashconsing of projections, | Matthieu Sozeau | |
| resulting in huge speedup at Qed/section closing in presence of primitive projections. | |||
| 2014-12-17 | Fixing bug #3796. | Pierre-Marie Pédrot | |
| 2014-12-17 | Fixing Makefile so that it puts the -thread flag on the right place. | Pierre-Marie Pédrot | |
| 2014-12-17 | Update checker/values and cic due to changes in case_info and record_body. | Matthieu Sozeau | |
| 2014-12-17 | Future: blocking by default | Enrico Tassi | |
| 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. | |||
| 2014-12-17 | STM: resilient on errors in non delegated proofs | Enrico Tassi | |
| 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). | |||
| 2014-12-17 | CoqIDE: cleanup jobs window on worker death | Enrico Tassi | |
| 2014-12-17 | STM: rename and simplify flags | Enrico Tassi | |
| 2014-12-17 | STM: simplify state management | Enrico Tassi | |
| 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. | |||
| 2014-12-17 | AsyncTaskQueue: simpler model (no parking area, continuation tasks) | Enrico Tassi | |
| 2014-12-17 | WorkerPool: simpler fuctor and no more parking area | Enrico Tassi | |
| 2014-12-17 | TQueue: a way to unblock threads begin destroyed waiting on pop | Enrico Tassi | |
| 2014-12-17 | Spawn: fix request of Gc statistics | Enrico Tassi | |
| 2014-12-17 | CThread: use a different type for thread friendly in_channels | Enrico Tassi | |
| 2014-12-17 | Summary: more surgery functions | Enrico Tassi | |
| API to let one forge a frozen state out of another frozen state plus some frozen bits | |||
| 2014-12-17 | Global: export the name of the summary entry | Enrico Tassi | |
| 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) | |||
| 2014-12-17 | Dyn: add API to check of two Dyn.t are == | Enrico Tassi | |
| A Dyn.t boxes a type tag with the original object, so calling == on the Dyn.t does not work, hence this extra API. | |||
| 2014-12-17 | Arguments: warn only if no option is given (Close 3860) | Enrico Tassi | |
| 2014-12-17 | CoqIDE: better messages | Enrico Tassi | |
| 2014-12-17 | Revert and correctly fix "#4843 part 2 : The .cmxs files for plugins must ↵ | Pierre Boutillier | |
| have x permission" This reverts commit 607503b28fca50f4b76b2237d5ca13802b8252fa. | |||
| 2014-12-16 | #3828 is solved. | Hugo Herbelin | |
| 2014-12-16 | Moving #2447 (congruence) to fixed. | Hugo Herbelin | |
| 2014-12-16 | In CHANGES, alerting about stronger check on notation level modifiers. | Hugo Herbelin | |
| 2014-12-16 | More printers for ltac signatures. | Hugo Herbelin | |
| 2014-12-16 | Test for #3654. | Hugo Herbelin | |
| 2014-12-16 | fix bug #2447 in congruence | Pierre Corbineau | |
| 2014-12-16 | fix bug #2447 in congruence | Pierre Corbineau | |
| 2014-12-16 | Fixing CAMLP4 compilation. | Pierre-Marie Pédrot | |
| 2014-12-16 | msg_info now puts infomsg tag in emacs mode. | Pierre Courtieu | |
| Fixes the idtac "string" not appearing in proofgeneral because printined *before* the goal. | |||
| 2014-12-16 | Proper thread-safe implementation for Exninfo. | Pierre-Marie Pédrot | |
| This is the second part of the Exninfo patch. It introduces dependency in the Thread library in all Coq files. | |||
| 2014-12-16 | Getting rid of Exninfo hacks. | Pierre-Marie Pédrot | |
| 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. | |||
| 2014-12-16 | Error messages of Searchxxx are coherent with goal selector. | Pierre Courtieu | |
| 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. | |||
| 2014-12-16 | Fix for #3154: use CUnix.sys_command to call native compiler. | Maxime Dénès | |
| Patch by CJ on bugzilla. CUnix.sys_command doesn't rely on a shell, so extra care with cmd.exe vs sh is no longer required. | |||
| 2014-12-15 | Changed bullet informations to warning for better display in PG. | Pierre Courtieu | |
| Since it displays together with the goal, it is better (for pg and other interfaces probably) that they are in a different message. | |||
| 2014-12-15 | Adapted test file for About. | Pierre Courtieu | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |