aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm
Commit message (Expand)AuthorAge
* Fix for #4603, part 3: definitions inside proofs not handled properly by coqc.Gravatar Maxime Dénès2016-05-04
* Build stm debugging messages lazily so that they are not silentlyGravatar Hugo Herbelin2016-04-15
* Quick fix for #4603 (part 2): Anomaly: Universe undefinedGravatar Maxime Dénès2016-04-12
* Univs: fix get_current_context (bug #4603, part I)Gravatar Matthieu Sozeau2016-03-25
* Tentative fix for bug #4614: "Fully check the document" is uninterruptable.Gravatar Pierre-Marie Pédrot2016-03-15
* Rename Ephemeron -> CEphemeron.Gravatar Maxime Dénès2016-03-04
* STM: Print/Extraction have to be skipped if -quickGravatar Enrico Tassi2016-02-19
* STM: classify some variants of Instance as regular `Fork nodes.Gravatar Enrico Tassi2016-02-19
* STM: always stock in vio files the first node (state) of a proofGravatar Enrico Tassi2016-02-10
* STM: not delegate proofs that contain Vernac(Module|Require|Import), #4530Gravatar Enrico Tassi2016-02-10
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.Gravatar Maxime Dénès2016-01-15
* fixup d2b468a, evar normalization is neededGravatar Enrico Tassi2016-01-04
* par: check if the goal is not ground and fail (fix #4465)Gravatar Enrico Tassi2016-01-04
* workers: purge short version of -load-vernac too (fix #4458)Gravatar Enrico Tassi2016-01-04
* vio: fix argument parsing (progress on #4442)Gravatar Enrico Tassi2015-12-01
* Univs: correctly register universe binders for lemmas.Gravatar Matthieu Sozeau2015-11-28
* Follow-up fix on Enrico's 6e376c8097d75b6e, with Enrico.Gravatar Maxime Dénès2015-11-02
* STM: fix undo into a branch containing side effectsGravatar Enrico Tassi2015-11-02
* STM: never reopen a branch containing side effectsGravatar Enrico Tassi2015-11-02
* Add a way to get the right fix_exn in external vernacular commandsGravatar Matthieu Sozeau2015-10-30
* Handle side-effects of Vernacular commands inside proofs better, so thatGravatar Matthieu Sozeau2015-10-29
* Avoid type checking private_constants (side_eff) again during Qed (#4357).Gravatar Enrico Tassi2015-10-28
* Miscellaneous typos, spacing, US spelling in comments or variable names.Gravatar Hugo Herbelin2015-10-18
* When typechecking a lemma statement, try to resolve typeclasses beforeGravatar Matthieu Sozeau2015-10-14
* STM: Work around an occasional crash in dot (debug output)Gravatar Alec Faithfull2015-10-09
* TQueue: Allow some tasks to be saved when clearing a TQueueGravatar Alec Faithfull2015-10-09
* TQueue: Expose the length of TQueuesGravatar Alec Faithfull2015-10-09
* STM: Added functions for saving and restoring the internal stateGravatar Alec Faithfull2015-10-09
* STM: Pass exception information to unreachable_state_hook functionsGravatar Alec Faithfull2015-10-09
* Axioms now support the universe binding syntax.Gravatar Pierre-Marie Pédrot2015-10-08
* Proof using: let-in policy, optional auto-clear, forward closure*Gravatar Enrico Tassi2015-10-08
* Spawn: use each socket exclusively for writing or readingGravatar Enrico Tassi2015-10-08
* STM: for PIDE based UIs, edit_at requires no Reach.known_stateGravatar Enrico Tassi2015-10-08
* STM: fix backtrace handlingGravatar Enrico Tassi2015-10-08
* Univs: fix semantics of Type in proof mode in universe-polymorphic modeGravatar Matthieu Sozeau2015-10-02
* Univs: fix handling of side effects/delayed proofsGravatar Matthieu Sozeau2015-10-02
* Univs: fix many evar_map initializations and leaks.Gravatar Matthieu Sozeau2015-10-02
* Remove some uses of Loadpath.get_paths.Gravatar Guillaume Melquiond2015-09-29
* STM: Reset takes Ltac <ident> into account (Close #4316)Gravatar Enrico Tassi2015-09-15
* Univs: Add universe binding lists to definitionsGravatar Matthieu Sozeau2015-09-14
* STM: save a full state for queries.Gravatar Enrico Tassi2015-09-01
* Removing code duplication in Lemmas.Gravatar Pierre-Marie Pédrot2015-08-19
* Documentation by giving a name to a large type.Gravatar Pierre-Marie Pédrot2015-08-19
* STM: make multiple, admitted, nested proofs work (fix #4314)Gravatar Enrico Tassi2015-07-30
* STM: emit a warning when a QED/Admitted proof contains a nested lemmaGravatar Enrico Tassi2015-07-30
* STM: fix backtrack in presence of nested, immediate, proofsGravatar Enrico Tassi2015-07-30
* STM: remove assertion not being true for nested, immediate, proofs (#4313)Gravatar Enrico Tassi2015-07-30
* Fixing what seems to be a typo.Gravatar Hugo Herbelin2015-07-29
* ShowScript: as 8.4 w.r.t. unnamed proofs and non tactic vernacs (fix #4308)Gravatar Enrico Tassi2015-07-28
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 02:52:46 +0000