| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-09-19 | Add XML protocol support for Wait. | Maxime Dénès | |
| 2017-09-15 | Merge PR #1042: Fixing minor typos in stm/coqide | Maxime Dénès | |
| 2017-09-11 | Typo in the header of ide_slave.ml. | Hugo Herbelin | |
| 2017-09-11 | Coqide: adding a separating space in some debugging messages. | Hugo Herbelin | |
| This prevents seeing things like MsgDirectory which are actually intended to be two distinct words. | |||
| 2017-09-06 | use get_arguments, String.concat, remove -I | Paul Steckler | |
| 2017-09-05 | read flags from project file for Compile Buffer | Paul Steckler | |
| 2017-08-23 | Fix BZ#5687: Coqtop died badly modal message box from CoqIDE. | Pierre-Marie Pédrot | |
| We let the user choose the most appropriate action to do if coqtop decides to go berserk. | |||
| 2017-08-08 | Set detachable windows type hint to dialog. | Olivier Marty | |
| Windows such as Search & Replace are dialogs. For some window managers, the hint changes how the window is displayed. | |||
| 2017-08-01 | Merge PR #919: Remove a few useless evar-normalizations in printing code. | Maxime Dénès | |
| 2017-07-31 | Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t instead | Maxime Dénès | |
| 2017-07-28 | Merge PR #823: Async off in Windows by default in CoqIDE | Maxime Dénès | |
| 2017-07-27 | deprecate Pp.std_ppcmds type alias | Matej Košík | |
| 2017-07-26 | Remove a few useless evar-normalizations in printing code. | Pierre-Marie Pédrot | |
| 2017-07-04 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2017-07-04 | Bump year in headers. | Pierre-Marie Pédrot | |
| 2017-06-26 | disable async on Windows by default | Paul Steckler | |
| 2017-06-21 | [ide] Correct more merging errors. | Emilio Jesus Gallego Arias | |
| This file doesn't want to leave us. | |||
| 2017-06-20 | Default colors for CoqIDE are actually applied. | Cyprien Mangin | |
| This fixes bug #5380 in particular. More generally, tags were not updated to the correct default value if the corresponding line in the configuration file was missing. | |||
| 2017-06-20 | Merge PR#774: [ide] Add route_id parameter to query call. | Maxime Dénès | |
| 2017-06-19 | Merge PR#795: [ide] Better exn printing. [fixes BZ#5524] | Maxime Dénès | |
| 2017-06-19 | Change CoqIDE-specific to neutral wording | Paul Steckler | |
| 2017-06-18 | [ide] Add route_id parameter to query call. | Emilio Jesus Gallego Arias | |
| 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 ####. | |||
| 2017-06-18 | [ide] Better exn printing. [fixes BZ#5524] | Emilio Jesus Gallego Arias | |
| Due to the situation explained in bug 5360, error printing in ide_slave results in an anomaly. We fix that by properly processing the error. This fixes BZ#5524, however BZ#5525 , still applies. | |||
| 2017-06-16 | Fix bugs and add an option for cumulativity | Amin Timany | |
| 2017-06-02 | Drop '.' from CErrors.anomaly, insert it in args | Jason Gross | |
| 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 ``` | |||
| 2017-06-01 | Bump year in headers. | Maxime Dénès | |
| 2017-05-30 | [ide] Correct merging error. | Emilio Jesus Gallego Arias | |
| There was a mistake in the conflict resolution of merge 6f2c19a1054ce58927dfa5b33131c3665fd5fdf8 which wrongly undid the the deletion of the file `ide/texmacspp.ml` in 6a412da , fixing here and sorry for the problem. | |||
| 2017-05-30 | Merge PR#356: Making management of installation directories more structured, ↵ | Maxime Dénès | |
| more uniform | |||
| 2017-05-29 | Relying on computation done in Envars to discover the installation directories. | Hugo Herbelin | |
| This allows to share the test for possible relocalisation done in envars.ml. | |||
| 2017-05-29 | Configuration: always giving a value to configdir and datadir. | Hugo Herbelin | |
| They were not used for looking for coqide files in the situation when the effective installation path happens to be exactly the installation path proposed by default, while relevant files were however (possibly) installed in these directories. | |||
| 2017-05-28 | Fail on deprecated warning even for Ocaml > 4.02.3 | Gaëtan Gilbert | |
| Deprecations which can't be fixed in 4.02.3 are locally wrapped with [@@@ocaml.warning "-3"]. The only ones encountered are - capitalize to capitalize_ascii and variants. Changing to ascii would break coqdoc -latin1 and maybe other things though. - external "noalloc" to external [@@noalloc] | |||
| 2017-05-25 | Merge PR#481: [option] Remove support for non-synchronous options. | Maxime Dénès | |
| 2017-05-25 | Merge PR#406: coq makefile2 | Maxime Dénès | |
| 2017-05-24 | Merge branch 'trunk' into located_switch | Emilio Jesus Gallego Arias | |
| 2017-05-24 | [option] Remove support for non-synchronous options. | Emilio Jesus Gallego Arias | |
| Inspired by https://coq.inria.fr/bugs/show_bug.cgi?id=5229 , which this PR solves, I propose to remove support for non-synchronous options. It seems the few uses of `optsync = false` we legacy and shouldn't have any impact. Moreover, non synchronous options may create particularly tricky situations as for instance, they won't be propagated to workers. | |||
| 2017-05-23 | CoqProject_file: API and code cleanup (tuples -> records) | Enrico Tassi | |
| 2017-05-23 | ide/project_file.ml4 -> lib/coqProject_file.ml4 + .mli | Enrico Tassi | |
| The .mli only acknowledges the current API. I'm not guilty your honor! | |||
| 2017-05-23 | ide/project_fie.ml4: include standard banner with copyright | Enrico Tassi | |
| 2017-05-23 | [vernac] Remove `Save.` command. | Emilio Jesus Gallego Arias | |
| It has been deprecated for a while in favor of `Qed`. | |||
| 2017-05-18 | [ide] Disable `print_ast` call. | Emilio Jesus Gallego Arias | |
| So far this part of the system has shown little utility other than having developers put time to fix it every time they change something in the system. I have never seen this functionality used in the wild, and a large part of the vernac was marked TODO. Given that we have automatic methods to provide this functionality these days (PPX), we remove Texmacspp. | |||
| 2017-05-04 | labelizing arguments | Pierre Courtieu | |
| 2017-05-04 | Adding an option "Printing Unfocused". | Pierre Courtieu | |
| Off by default. + small refactoring of emacs hacks in printer.ml. | |||
| 2017-05-02 | Merge PR#582: Fix warnings | Maxime Dénès | |
| 2017-04-28 | Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of ↵ | Maxime Dénès | |
| let-ins | |||
| 2017-04-27 | Remove uses of [Flags.make_silent] | Gaetan Gilbert | |
| 2017-04-27 | Warning 29: non escaped end of line may be non portable | Gaetan Gilbert | |
| 2017-04-27 | Remove some unused values and types | Gaetan Gilbert | |
| 2017-04-27 | Use [method!] to override methods (warning 7) | Gaetan Gilbert | |
| 2017-04-27 | Fix omitted labels in function calls | Gaetan Gilbert | |
| 2017-04-25 | [location] [ast] Switch Constrexpr AST to an extensible node type. | Emilio Jesus Gallego Arias | |
| Following @gasche idea, and the original intention of #402, we switch the main parsing AST of Coq from `'a Loc.located` to `'a CAst.ast` which is private and record-based. This provides significantly clearer code for the AST, and is robust wrt attributes. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |