aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm
Commit message (Expand)AuthorAge
* Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* typosGravatar Enrico Tassi2016-05-23
* Put the "cofix" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* Put the "fix" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* Proof_global, STM: cleanup + use default_proof_mode instead of "Classic"Gravatar Enrico Tassi2016-05-10
* STM: code cleanupGravatar Enrico Tassi2016-05-10
* Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-04
|\
| * Fix for #4603, part 3: definitions inside proofs not handled properly by coqc.Gravatar Maxime Dénès2016-05-04
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-04-24
|\|
| * 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
* | Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...Gravatar Matthieu Sozeau2016-04-04
|\ \
* \ \ Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-30
|\ \ \ | | |/ | |/|
| * | Univs: fix get_current_context (bug #4603, part I)Gravatar Matthieu Sozeau2016-03-25
* | | Moving the Ltac definition command to an EXTEND based command.Gravatar Pierre-Marie Pédrot2016-03-20
* | | Moving Tactic Notation to an EXTEND based command.Gravatar Pierre-Marie Pédrot2016-03-20
* | | Moving VernacSolve to an EXTEND-based definition.Gravatar Pierre-Marie Pédrot2016-03-19
* | | Removing the dependency in VernacSolve in the STM.Gravatar Pierre-Marie Pédrot2016-03-19
* | | Relying on Vernac classifier to flag tactics in the STM.Gravatar Pierre-Marie Pédrot2016-03-19
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-18
|\| |
| * | Tentative fix for bug #4614: "Fully check the document" is uninterruptable.Gravatar Pierre-Marie Pédrot2016-03-15
* | | Supporting "(@foo) args" in patterns, where "@foo" has no arguments.Gravatar Hugo Herbelin2016-03-13
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-05
|\| |
| * | Rename Ephemeron -> CEphemeron.Gravatar Maxime Dénès2016-03-04
* | | 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