| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-09-12 | Uniformisation of the order of arguments env and sigma. | Hugo Herbelin | |
| 2014-09-10 | VernacExtend does not dispatch on type anymore. | Pierre-Marie Pédrot | |
| 2014-09-09 | Marshalling errors should be bold and red (should never happen actually) | Enrico Tassi | |
| 2014-09-09 | A marshalling failure does not make a worker `Old | Enrico Tassi | |
| 2014-09-09 | Back: print subgoals as in 8.4 (Close: 3585) | Enrico Tassi | |
| 2014-09-09 | BackTo not part of the doc when used by emacs | Enrico Tassi | |
| Used to work "by chance". | |||
| 2014-09-09 | Undo: if the ui is coqtop (command line) then Undo is not part of the doc. | Enrico Tassi | |
| 2014-09-09 | Dropped proofs (Abort) are evaluated synchronously (Closes: 3550, 3407) | Enrico Tassi | |
| 2014-09-04 | Remove [Infer] option of records. | Arnaud Spiwack | |
| Dead code formerly used by the now defunct [autoinstances]. | |||
| 2014-09-04 | Print [Variant] types with the keyword [Variant]. | Arnaud Spiwack | |
| Involves changing the [mind_finite] field in the kernel from a bool to the trivalued type [Decl_kinds.recursivity_kind]. This is why so many files are (unfortunately) affected. It would not be very surprising if some bug was introduced. | |||
| 2014-09-02 | stm: use xlabel insted of label in dot (debug) output | Enrico Tassi | |
| 2014-09-02 | coqworkmgr | Enrico Tassi | |
| 2014-08-26 | Do not pass "-batch" or "-load-vernac-source" to slaves, avoiding errors in | Matthieu Sozeau | |
| stm test-suite files. | |||
| 2014-08-05 | STM: new "par:" goal selector, like "all:" but in parallel | Enrico Tassi | |
| par: distributes the goals among a number of workers given by -async-proofs-tac-j (defaults to 2). | |||
| 2014-08-05 | STM: code restructured to reuse task queue for tactics | Enrico Tassi | |
| 2014-08-05 | STM: Classify Let as non asynchronous (Closes: #3486) | Enrico Tassi | |
| 2014-08-04 | STM: when looking up in the cache catch Expired exc | Carst Tankink | |
| 2014-08-04 | STM: generate Feedback message for parsing errors | Enrico Tassi | |
| 2014-08-04 | STM: use a real priority queue | Enrico Tassi | |
| 2014-08-04 | STM: encapsulate Pp.message in Feedback.feedback | Carst Tankink | |
| 2014-08-04 | STM: VtQuery holds the id of the state it refers to | Carst Tankink | |
| 2014-07-29 | STM: print goals with no duplicates | Enrico Tassi | |
| 2014-07-16 | Fixing universe substitution in mutual fixpoints. | Pierre-Marie Pédrot | |
| 2014-07-16 | STM: check-vi-task fixed | Enrico Tassi | |
| 2014-07-16 | STM: Goal printing got wrong in a merge, fixed | Enrico Tassi | |
| 2014-07-11 | STM: let toploop plugins specify the flags for STM workers | Enrico Tassi | |
| 2014-07-11 | STM: flag to turn off branch reopening | Enrico Tassi | |
| This is useful if a UI does not support that | |||
| 2014-07-11 | STM: add optionally takes the id of the new tip | Enrico Tassi | |
| 2014-07-11 | STM: export the observe function (useful for pide) | Enrico Tassi | |
| 2014-07-11 | Feedback: LoadedFile + Goals | Enrico Tassi | |
| LoadedFile is generated when a .vo is loaded Goals is generated when -feedback-goals | |||
| 2014-07-10 | Better handling of the universe context in case of Admitted proof obligations. | Matthieu Sozeau | |
| 2014-07-10 | option to always delegate futures to workers | Enrico Tassi | |
| 2014-07-10 | more APIs in TQueue and CThread | Enrico Tassi | |
| These are now sufficient to implement PIDE | |||
| 2014-07-01 | Add toplevel commands to declare global universes and constraints. | Matthieu Sozeau | |
| 2014-07-01 | Patch from Enrico Tassi to get Drop compatible with stm. | Enrico Tassi | |
| 2014-06-28 | Typo in stm error message. | Hugo Herbelin | |
| 2014-06-25 | all coqide specific files moved into ide/ | Enrico Tassi | |
| lib/interface split into: - lib/feedback subscribe-based feedback bus (also used by coqidetop) - ide/interface definition of coqide protocol messages lib/pp structured info/err/warn messages lib/serialize split into: - lib/serialize generic xml serialization (list, pairs, int, loc, ...) used by coqide but potentially useful to other interfaces - ide/xmlprotocol serialization of protocol messages as in ide/interface the only drawback is that coqidetop needs -thread and I had to pass that option to all files in ide/ | |||
| 2014-06-25 | cut toploop(s) out of coqtop: now they are loaded dynamically | Enrico Tassi | |
| User interface writers can drop a footop.cmxs in $(COQLIB)/toploop/ and pass -toploop footop to customize the coq main loop. A toploop must set Coqtop.toploop_init and Coqtop.toploop_run to functions respectively initializing the toploop (and parsing toploop specific arguments) and running the main loop itself. For backward compatibility -ideslave and -async-proofs worker do set the toploop to coqidetop and stmworkertop respectively. | |||
| 2014-06-23 | Fix handling of side effects in Defined objects (Closes: HoTT#111 + 3344) | Enrico Tassi | |
| Every time you use abstract a kitten dies, please stop. | |||
| 2014-06-18 | Proofs now take and return an evar_universe_context, simplifying interfaces | Matthieu Sozeau | |
| and avoiding explicit substitutions and merging of contexts, e.g. in obligations.ml. The context produced by typechecking a statement is passed in the proof, allowing the universe name context to be correctly folded as well. Mainly an API cleanup. | |||
| 2014-06-17 | Removing dead code. | Pierre-Marie Pédrot | |
| 2014-06-08 | Moving hook code from Future to Lemmas. This seemed to disrupt compilation of | Pierre-Marie Pédrot | |
| the checker, and it was not used before that anyway. | |||
| 2014-06-08 | Enforce a correct exception handling in declaration_hooks | Enrico Tassi | |
| This should finally get rid of the following class of bugs: Qed fails, STM undoes to the beginning of the proof because the exception is not annotated with the correct state, PG gets out of sync because errors always refer to the last command in PGIP. | |||
| 2014-06-08 | STM: handle "Time Abort" correctly (Closes: 3332) | Enrico Tassi | |
| 2014-06-06 | Remove the syntax [Vernac1. Vernac2. … Vernacn. ]. | Arnaud Spiwack | |
| It grouped a list of vernac commands as a single one. It was undocumented and unused (and apparently unusable, because the intermediate '.' seem to be parsed as end of phrases by the interfaces). The main application could be to group the commands for Time. There is room for such an application in the syntax, but I unplugged the syntax for the time being. The syntax would conflict with the use of a standalone dispatching tactical [ t1 | t2 | … | tn ]. I took the opportunity to separate the code dedicated to lists of commands in a separate type from vernac_expr. | |||
| 2014-05-26 | - Fix in kernel conversion not folding the universe constraints | Matthieu Sozeau | |
| correctly when comparing stacks. - Disallow Type i <= Prop/Set constraints, that would otherwise allow constraints that make a universe lower than Prop. - Fix stm/lemmas that was pushing constraints to the global context, it is done depending on the constant/variable polymorphic status now. - Adapt generalized rewriting in Type code to these fixes. | |||
| 2014-05-15 | poly: remove unused attribute to STM nodes and vernac classificaiton | Enrico Tassi | |
| 2014-05-15 | Polymorphic Lemmas are like Defined ones for STM | Enrico Tassi | |
| 2014-05-06 | - Fix bug preventing apply from unfolding Fixpoints. | Matthieu Sozeau | |
| - Remove Universe Polymorphism flags everywhere. - Properly infer, discharge template arities and fix substitution inside them (kernel code to check for correctness). - Fix tactics that were supposing universe polymorphic constants/inductives to be parametric on that status. Required to make interp_constr* return the whole evar universe context now. - Fix the univ/level/instance hashconsing to respect the fact that marshalling doesn't preserve sharing, sadly losing most of its benefits. Short-term solution is to add hashes to these for faster comparison, longer term requires rewriting all serialization code. Conflicts: kernel/univ.ml tactics/tactics.ml theories/Logic/EqdepFacts.v | |||
| 2014-05-06 | Adapt universe polymorphic branch to new handling of futures for delayed proofs. | Matthieu Sozeau | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |