index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
stm
/
stm.ml
Commit message (
Expand
)
Author
Age
...
*
Safer API for Global.body_of_constant and variants.
Pierre-Marie Pédrot
2017-07-13
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
Merge PR#821: [vernac] Remove stale bool parameter from `VernacStartTheoremPr...
Maxime Dénès
2017-06-23
|
\
*
\
Merge PR#815: STM: par: report no error to UIs in non-solve mode
Maxime Dénès
2017-06-23
|
\
\
|
|
*
[vernac] Remove stale bool parameter from `VernacStartTheoremProof`
Emilio Jesus Gallego Arias
2017-06-21
*
|
|
[stm] Fix route setting on VtQuery
Emilio Jesus Gallego Arias
2017-06-20
|
|
/
|
/
|
|
*
STM: par: report no error to UIs in non-solve mode
Enrico Tassi
2017-06-20
*
|
[ide] Add route_id parameter to query call.
Emilio Jesus Gallego Arias
2017-06-18
|
/
*
Merge PR#748: [stm] More fixes for nested commands [bugzilla 5589]
Maxime Dénès
2017-06-15
|
\
*
|
[proof] Deprecate redundant wrappers.
Emilio Jesus Gallego Arias
2017-06-11
|
*
[stm] More fixes for nested commands [bugzilla 5589]
Emilio Jesus Gallego Arias
2017-06-07
|
/
*
Merge PR#717: [proof] Deprecate "proof mode" API
Maxime Dénès
2017-06-07
|
\
*
|
Remove the Sigma (monotonous state) API.
Maxime Dénès
2017-06-06
*
|
Merge PR#716: Don't double up on periods in anomalies
Maxime Dénès
2017-06-06
|
\
\
*
|
|
[stm] Solve bug 5577 "STM branch name is incorrect with Time"
Emilio Jesus Gallego Arias
2017-06-03
|
*
|
Drop '.' from CErrors.anomaly, insert it in args
Jason Gross
2017-06-02
|
/
/
*
|
[emacs] [toplevel] Make emacs flag local to the toplevel.
Emilio Jesus Gallego Arias
2017-06-01
|
*
[proof] Deprecate "proof mode" API
Emilio Jesus Gallego Arias
2017-05-31
|
/
*
[stm] Rename Side-Effect type.
Emilio Jesus Gallego Arias
2017-05-27
*
[stm] Uniformize `Sideff / Sideff.
Emilio Jesus Gallego Arias
2017-05-27
*
Merge PR#645: [stm] Tweak debug options.
Maxime Dénès
2017-05-25
|
\
*
\
Merge branch 'trunk' into located_switch
Emilio Jesus Gallego Arias
2017-05-24
|
\
\
|
|
*
[stm] Tweak debug options.
Emilio Jesus Gallego Arias
2017-05-18
|
|
/
|
*
Fix 4.04 warnings
Gaetan Gilbert
2017-04-27
|
*
Remove unused constructors
Gaetan Gilbert
2017-04-27
|
*
Remove some unused values and types
Gaetan Gilbert
2017-04-27
|
*
Fix omitted labels in function calls
Gaetan Gilbert
2017-04-27
*
|
[location] Make location optional in Loc.located
Emilio Jesus Gallego Arias
2017-04-25
*
|
[location] Remove Loc.ghost.
Emilio Jesus Gallego Arias
2017-04-25
|
/
*
Merge branch 'v8.6' into trunk
Maxime Dénès
2017-04-15
|
\
|
*
Merge PR#510: Correctly identify [Time Defined.] as a defined
Maxime Dénès
2017-04-12
|
|
\
*
|
\
Merge PR#441: Port Toplevel to the Stm API
Maxime Dénès
2017-04-12
|
\
\
\
|
*
|
|
[toplevel] [stm] cleanup in module open
Emilio Jesus Gallego Arias
2017-04-12
|
*
|
|
[stm] [nit] Centralize compile-time debug flag.
Emilio Jesus Gallego Arias
2017-04-12
|
*
|
|
[stm] Improve error messages on add/parse.
Emilio Jesus Gallego Arias
2017-04-12
|
*
|
|
[stm] Port the toplevel to the STM.
Emilio Jesus Gallego Arias
2017-04-12
|
*
|
|
[stm] Move main parsing entry point to the STM.
Emilio Jesus Gallego Arias
2017-04-12
|
*
|
|
[stm] Remove edit_id.
Emilio Jesus Gallego Arias
2017-04-12
|
*
|
|
[stm] remove process_error_hook
Emilio Jesus Gallego Arias
2017-04-07
|
*
|
|
[stm] remove tactic_being_run hook
Emilio Jesus Gallego Arias
2017-04-07
|
|
*
|
Fix a few programming pearls related to Time, Fail and Redirect.
Maxime Dénès
2017-04-06
*
|
|
|
Merge branch 'trunk' into pr379
Maxime Dénès
2017-04-04
|
\
|
|
|
|
*
|
|
Merge branch 'v8.6' into trunk
Maxime Dénès
2017-03-30
|
|
\
|
|
|
|
*
|
Run non-tactic comands without resilient_command
Tej Chajed
2017-03-29
*
|
|
|
Merge branch 'trunk' into pr379
Maxime Dénès
2017-03-24
|
\
\
\
\
|
|
*
|
|
[stm] Remove some obsolete vernacs/classification.
Emilio Jesus Gallego Arias
2017-03-24
|
|
/
/
/
|
|
|
*
Correctly identify [Time Defined.] as a defined
Tej Chajed
2017-03-23
|
|
|
/
|
*
|
[pp] Remove uses of expensive string_of_ppcmds.
Emilio Jesus Gallego Arias
2017-03-21
|
*
|
[pp] [ide] Minor cleanups in pp code.
Emilio Jesus Gallego Arias
2017-03-21
|
*
|
[pp] Make feedback the only logging mechanism.
Emilio Jesus Gallego Arias
2017-03-21
[prev]
[next]