aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm
Commit message (Expand)AuthorAge
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-02-21
|\
| * 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
* | merging conflicts with the original "trunk__CLEANUP__Context__2" branchGravatar Matej Kosik2016-02-15
|\ \
* \ \ Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-02-13
|\ \ \ | | |/ | |/|
| * | 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
| | * CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
| |/ |/|
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * 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
* | CLEANUP: removing unnecessary wrapperGravatar Matej Kosik2016-01-11
* | CLEANUP: removing unused fieldGravatar Matej Kosik2016-01-11
* | Merge remote-tracking branch 'origin/v8.5' into trunkGravatar Guillaume Melquiond2016-01-05
|\|
| * 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
* | Remove some unused functions.Gravatar Guillaume Melquiond2016-01-02
* | Remove some useless module opening.Gravatar Guillaume Melquiond2016-01-02
* | Reduce dependencies of interface files.Gravatar Guillaume Melquiond2016-01-02
* | Remove unused functions.Gravatar Guillaume Melquiond2016-01-01
* | Remove useless recursive flags.Gravatar Guillaume Melquiond2016-01-01
* | CLEANUP: the definition of the "Constrexpr.case_expr" type was simplifiedGravatar Matej Kosik2015-12-18
* | CLEANUP: Vernacexpr.VernacDeclareTacticDefinitionGravatar Matej Kosik2015-12-18
* | CLEANUP: Removing "Vernacexpr.VernacNop" variant to which no Vernacular comma...Gravatar Matej Kosik2015-12-18
* | CLEANUP: Vernacexpr.vernac_exprGravatar Matej Kosik2015-12-18
* | Specializing the Dyn module to each usecase.Gravatar Pierre-Marie Pédrot2015-12-04
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-03
|\|
| * vio: fix argument parsing (progress on #4442)Gravatar Enrico Tassi2015-12-01
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-29
|\|
| * Univs: correctly register universe binders for lemmas.Gravatar Matthieu Sozeau2015-11-28
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-05
|\|
| * 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
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-30
|\|
| * 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
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-29
|\|
| * Avoid type checking private_constants (side_eff) again during Qed (#4357).Gravatar Enrico Tassi2015-10-28
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-19
|\|
| * Miscellaneous typos, spacing, US spelling in comments or variable names.Gravatar Hugo Herbelin2015-10-18
* | Clarifying and documenting the UState API.Gravatar Pierre-Marie Pédrot2015-10-17
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-15
|\|
| * When typechecking a lemma statement, try to resolve typeclasses beforeGravatar Matthieu Sozeau2015-10-14
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-10
|\|
| * 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