| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-12-23 | Vi2vo: fix handling of univ constraints coming from the body | Enrico Tassi | |
| 2014-12-23 | Minor modification of CHANGE. | Pierre Courtieu | |
| 2014-12-23 | A global [gfail] tactic which works like [fail] except that it fails even if ↵ | Arnaud Spiwack | |
| there is no focused goal. The 'g' is for "global". The arguments are the same as [fail]. Beware: [let x := constr:… in tac] is a goal-local operation regardless of whether [tac] is goal-local or not. | |||
| 2014-12-23 | Remove compatibility layer from Ltac's [fail]. | Arnaud Spiwack | |
| 2014-12-23 | Fix compilation error in some configurations. | Arnaud Spiwack | |
| This was due to the unqualified uses of "Lazy" being disambiguated in different manners. I just changed the constructor name to "Select". Fixes #3877. | |||
| 2014-12-21 | Dead code in Univ. | Pierre-Marie Pédrot | |
| 2014-12-19 | Win32: fix installer | Enrico Tassi | |
| Still unsure about .o file (should they be shipped for the native_compute machinery or .cmxs suffice?) | |||
| 2014-12-19 | Install .v and .glob files too | Enrico Tassi | |
| PIDE based user interfaces use glob files and source files to implement hyperlinks | |||
| 2014-12-19 | Add a backtracking version of Ltac's [match]. | Arnaud Spiwack | |
| [multimatch … with …] returns every possible successes: every matching branch and every successes of these matching branch, so that subsequent tactics can backtrack as well. | |||
| 2014-12-19 | When pretyping [uconstr] closures, don't use the local Ltac variable ↵ | Arnaud Spiwack | |
| environment. A closure is supposedly closed: all the relevant Ltac variables should be then. The last field [ltac_genargs], if I'm not mistaken, is there to represent the Ltac variables which are bound but not to something which makes sense in a term. They should be irrelevant at this point, since the uconstr has already been interpreted and these checks are supposed to have happened. (though I'm not entirely sure they do, it can be an interesting exercise to try and make [uconstr] behave weirdly) I'm not quite sure why it caused #3679, though. But it still seems to be solved. | |||
| 2014-12-19 | Fixing performance issue of checker validation. | Pierre-Marie Pédrot | |
| The validation process was passing most of its time in the construction of the name of the current context. | |||
| 2014-12-19 | Fixing checker representation of values. | Pierre-Marie Pédrot | |
| 2014-12-19 | update md5 sums to make "make check" work | Enrico Tassi | |
| 2014-12-19 | Fix sigsegv in checker | Enrico Tassi | |
| 2014-12-19 | Better doc and a few fixes for Proof using. | Enrico Tassi | |
| 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. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |