aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm
Commit message (Collapse)AuthorAge
* Merge PR #775: [toplevel] Remove long ago deprecated and NOOP options.Gravatar Maxime Dénès2017-08-01
|\
| * [toplevel] Remove long ago deprecated and NOOP options.Gravatar Emilio Jesus Gallego Arias2017-07-27
| | | | | | | | Minor clean up, no sense in having these as they do nothing.
* | deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
|/
* Removing a use of AUContext.instance in the STM.Gravatar Pierre-Marie Pédrot2017-07-13
| | | | | We only delay monomorphic proofs in quick mode, so that their universe context will always be empty.
* Safer API for Global.body_of_constant and variants.Gravatar Pierre-Marie Pédrot2017-07-13
| | | | | We aditionally return the abstract universe context inside the option. This is relatively painless as most uses were using the option as a boolean.
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Merge PR#821: [vernac] Remove stale bool parameter from ↵Gravatar Maxime Dénès2017-06-23
|\ | | | | | | `VernacStartTheoremProof`
* \ Merge PR#815: STM: par: report no error to UIs in non-solve modeGravatar Maxime Dénès2017-06-23
|\ \
| | * [vernac] Remove stale bool parameter from `VernacStartTheoremProof`Gravatar Emilio Jesus Gallego Arias2017-06-21
| | | | | | | | | | | | | | | `VernacStartTheoremProof` contained a stale bool parameter from 15 years ago, which is unused today.
* | | [stm] Fix route setting on VtQueryGravatar Emilio Jesus Gallego Arias2017-06-20
| |/ |/| | | | | | | | | This is a fix for a mistake in d8874dd855d748aaaf504890487ab15ffd7a677d , where we forgot to propagate the route parameter.
| * STM: par: report no error to UIs in non-solve modeGravatar Enrico Tassi2017-06-20
| | | | | | | | | | | | Used to report to the UI an Error feedback message whenever a worker was non making any progress. This is wrong since no-progress is fine (as long as one does not specify "solve")
* | Merge PR#774: [ide] Add route_id parameter to query call.Gravatar Maxime Dénès2017-06-20
|\ \
| * | [ide] Add route_id parameter to query call.Gravatar Emilio Jesus Gallego Arias2017-06-18
| |/ | | | | | | | | | | | | | | This is necessary in order for clients to identify the results of queries. This is a minor breaking change of the protocol, affecting only this particular call. This change is necessary in order to fix bug ####.
* / Fix bugs and add an option for cumulativityGravatar Amin Timany2017-06-16
|/
* Merge PR#748: [stm] More fixes for nested commands [bugzilla 5589]Gravatar Maxime Dénès2017-06-15
|\
* | [proof] Deprecate redundant wrappers.Gravatar Emilio Jesus Gallego Arias2017-06-11
| | | | | | | | | | | | | | | | | | As we would like to reduce the role of proof_global in future versions, we start to deprecate old compatibility aliases in `Pfedit` in favor of the real functions underlying the 8.5 proof engine. We also deprecate a couple of alias types and explicitly mark the few remaining uses of `Pfedit`.
| * [stm] More fixes for nested commands [bugzilla 5589]Gravatar Emilio Jesus Gallego Arias2017-06-07
|/
* Merge PR#717: [proof] Deprecate "proof mode" APIGravatar Maxime Dénès2017-06-07
|\
* | Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Reminder of (some of) the reasons for removal: - Despite the claim in sigma.mli, it does *not* prevent evar leaks, something like: fun env evd -> let (evd',ev) = new_evar env evd in (evd,ev) will typecheck even with Sigma-like type annotations (with a proof of reflexivity) - The API stayed embryonic. Even typing functions were not ported to Sigma. - Some unsafe combinators (Unsafe.tclEVARS) were replaced with slightly less unsafe ones (e.g. s_enter), but those ones were not marked unsafe at all (despite still being so). - There was no good story for higher order functions manipulating evar maps. Without higher order, one can most of the time get away with reusing the same name for the updated evar map. - Most of the code doing complex things with evar maps was using unsafe casts to sigma. This code should be fixed, but this is an orthogonal issue. Of course, this was showing a nice and elegant use of GADTs, but the cost/benefit ratio in practice did not seem good.
* | Merge PR#716: Don't double up on periods in anomaliesGravatar Maxime Dénès2017-06-06
|\ \
* | | [stm] Solve bug 5577 "STM branch name is incorrect with Time"Gravatar Emilio Jesus Gallego Arias2017-06-03
| | |
| * | Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
|/ / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | As per https://github.com/coq/coq/pull/716#issuecomment-305140839 Partially using ```bash git grep --name-only 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*[^\.!]")' | xargs sed s'/\(anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*\s*[^\.! ]\)\s*")/\1.")/g' -i ``` and ```bash git grep --name-only ' !"' | xargs sed s'/ !"/!"/g' -i ``` The rest were manually edited by looking at the results of ```bash git grep anomaly | grep '\.ml' | grep -v 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp\.\)\?(\(\(Pp.\)\?str\)\?\s*".*\(\.\|!\)")' | grep 'anomaly\($\|[^_]\)' | less ```
* | [emacs] [toplevel] Make emacs flag local to the toplevel.Gravatar Emilio Jesus Gallego Arias2017-06-01
| | | | | | | | | | We remove the emacs-specific printing code from the core of Coq, now `-emacs` is a printing flag controlled by the toplevel.
| * [proof] Deprecate "proof mode" APIGravatar Emilio Jesus Gallego Arias2017-05-31
|/ | | | | Any users of this API should coordinate with the ongoing work in PRs numbered #459 and #566.
* Merge PR#690: [stm] Uniformize `Sideff / Sideff.Gravatar Maxime Dénès2017-05-29
|\
| * [stm] Rename Side-Effect type.Gravatar Emilio Jesus Gallego Arias2017-05-27
| | | | | | | | As suggested by @gares, now the meaning becomes way clearer.
* | [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
| | | | | | | | | | | | | | | | | | | | | | | | | | This is the continuation of #244, we now deprecate `CErrors.error`, the single entry point in Coq is `user_err`. The rationale is to allow for easier grepping, and to ease a future cleanup of error messages. In particular, we would like to systematically classify all error messages raised by Coq and be sure they are properly documented. We restore the two functions removed in #244 to improve compatibility, but mark them deprecated.
| * [stm] Uniformize `Sideff / Sideff.Gravatar Emilio Jesus Gallego Arias2017-05-27
|/ | | | This is a minor cleanup.
* Merge PR#645: [stm] Tweak debug options.Gravatar Maxime Dénès2017-05-25
|\
* \ Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\ \
| | * [stm] Tweak debug options.Gravatar Emilio Jesus Gallego Arias2017-05-18
| |/ | | | | | | | | | | | | | | We allow for a dynamic setting of the STM debug flag, and we print some more information about the result of `process_transaction`. We also fix a printing bug due to mixing `Printf` and `Format`, which are not compatible.
| * Fix 4.04 warningsGravatar Gaetan Gilbert2017-04-27
| |
| * Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
| |
| * Remove unused constructorsGravatar Gaetan Gilbert2017-04-27
| |
| * Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
| |
| * Fix omitted labels in function callsGravatar Gaetan Gilbert2017-04-27
| |
* | [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
| | | | | | | | | | | | | | | | | | | | | | | | This completes the Loc.ghost removal, the idea is to gear the API towards optional, but uniform, location handling. We don't print <unknown> anymore in the case there is no location. This is what the test suite expects. The old printing logic for located items was a bit inconsistent as it sometimes printed <unknown> and other times it printed nothing as the caller checked for `is_ghost` upstream.
* | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
|/ | | | Now it is a private field, locations are optional.
* Merge PR#579: [flags] Deprecate is_silent/is_verbose in favor of single flag.Gravatar Maxime Dénès2017-04-24
|\
* | Remove VernacErrorGravatar Gaetan Gilbert2017-04-21
| |
| * [flags] Deprecate is_silent/is_verbose in favor of single flag.Gravatar Emilio Jesus Gallego Arias2017-04-21
|/ | | | | | | | | Today, both modes are controlled by a single flag, however this is a bit misleading as is_silent really means "quiet", that is to say `coqc -q` whereas "verbose" is Coq normal operation. We also restore proper behavior of goal printing in coqtop on quiet mode, thanks to @Matafou for the report.
* Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-04-15
|\
| * Fix anomaly when doing [all:Check _.] during a proof.Gravatar Gaetan Gilbert2017-04-14
| |
* | Silence a few OCaml warnings.Gravatar Guillaume Melquiond2017-04-13
| |
| * Merge PR#510: Correctly identify [Time Defined.] as a definedGravatar Maxime Dénès2017-04-12
| |\
* | \ Merge PR#441: Port Toplevel to the Stm APIGravatar Maxime Dénès2017-04-12
|\ \ \
| * | | [toplevel] [stm] cleanup in module openGravatar Emilio Jesus Gallego Arias2017-04-12
| | | |
| * | | [stm] [nit] Centralize compile-time debug flag.Gravatar Emilio Jesus Gallego Arias2017-04-12
| | | |
| * | | [stm] Improve error messages on add/parse.Gravatar Emilio Jesus Gallego Arias2017-04-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | As suggested by @psteckler in #524 , we give more explicit information about what is wrong. We also provide some debug information for the possible dangerous case of having the tip go out of sync with the real installed state (which will make parsing fail if there was some changes to the parser). We also fix a couple of typos noticed by Paul, thanks Paul.
| * | | [stm] Port the toplevel to the STM.Gravatar Emilio Jesus Gallego Arias2017-04-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - We clean-up `Vernac` and make it use the STM API. - Now functions in `Vernac` for use in the toplevel and compiler take an starting `Stateid.t`. - Duplicated `Stm.interp` entry point is removed. - The XML protocol call `interp` is disabled.