aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2013-10-01STM: fix reporting of ongoing tasksgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16828 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-01STM: exceptions caming from slaves are now localizedgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16827 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-01CoqIDE: do not fail hard if a message is asynchronousgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16826 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-01STM: Unix.kill can failgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16825 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-01CoqIDE: fix reset initialgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16824 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30CoqIDE: use #present to raise error windowgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16823 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30Backtrace.record_backtrace in CoqIDE toogareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16822 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30CoqIDE: wg_Tooltip removed, new tooltip handlinggareuselesinge
- tooltips are attached to sentences - to find the tooltip text one goes back until the first start of sentence mark, finds the corresponding sentence and displays the tooltip - focused editing does not invalidate tooltips this way, since the text, its tags and marks is moved around consistently git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16821 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30STM: better handle proof modesgareuselesinge
Proof modes are really spaghetti code. It is a global state that you can't access (held by G_vernac). We stick it to the branches... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16820 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30fake_ide: call Coq.init as the first actiongareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16819 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30ideutils: stock_to_widget was ignoring the ~size argumentgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16818 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30wg_Command: detachable, less "from the 80s", query panegareuselesinge
- Tabs have labels derived from the query (e.g. "About eq_ind" will have "eq_ind" as its label, that is better than "Page 1" ;-) - Tabs have a [x] close icon - Icon to create a new tab in in the notebook - Dispotically grab the F1 key to open/close the query pane (alt-esc is grabbed by windows managers these days) - Esc hides the query pane (like the search pane) - F1 puts a detached query pane in front - Tab switches from the combo-box to the entry on its right - Detaching is taken-over, and the query pane is reparented in a regular window that can be resized - A detached query pane can be put back by closing the window git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16817 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30wg_Session: fix copy/paste of tagged textgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16816 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30STM: some refactoring, support revised CoqIDE protocolgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16815 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30CoqIDE ported to the revides protocolgareuselesinge
- the zone to be edited is now between the marks start_of_input and stop_of_input - when -debug is given, the edit zone is underlined - the cmd_stack is focused/unfocused according to the new protocol - read only tag resurrected and used to block the "Qed" ending a focused zone git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16814 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30fake_ide ported to the new protocol (FIXME tests fail)gareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16813 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30CoqIDE protocol/serialization revisedgareuselesinge
- both requests and responses are serialized using the same generic code - no more interp message. Replaced by: - query: performs a query (Search/Check...) at a given state - add: adds to the document a new sentence at the current edit point - edit_at: changes the edit point. the result could be a rewind _or_ a focus to a specific zone that can be edited without rewinding the whole document git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16812 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30lib/cstack: various improvementsgareuselesinge
- renaming reflecting the semantic of functions - ability to edit the stack at the top of a _focused_zone_ git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16811 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30lib/vcs: various improvementsgareuselesinge
- gc function to clear unreferenced nodes - utility function to get the ancestors of a commit - utility function to edit a merge commit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16810 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30lib/dag: various improvementsgareuselesinge
- clusters can hold some data - edges and nodes can be deleted git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16809 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30lib/future: computations that are Exn can be replacedgareuselesinge
A computation that is an exception morally holds no value hence can be replaced by an type-equivalent computation. This mechanism is used to edit broken proofs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16808 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-28Made rewrite tactic strategies pure. They were using quite uglilyppedrot
references. Now they carry around their state explicitly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16807 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-27Removing a bunch of generic equalities.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16806 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-26Opacifying the type of strategies.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16805 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-26Splitting Rewrite into a code part and a CAMLP4-dependent one.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16804 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-25Removing useless evar-related stuff.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16803 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-24Adding evar printing to debugger.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16802 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-24Fixing ocamldebug compilation by adding thread linking.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16801 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-20Fix name clash in "failure/inductive.v".xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16800 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-20Merge "circular_subtyping?.v" tests into a single "circular_subtyping.v" test.xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16799 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-20Merge "inductive?.v" tests into a single "inductive.v" test.xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16798 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-20Get rid of "shouldsucceed" subdirectory by moving tests to parent directory.xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16797 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-20Get rid of "shouldfail" subdirectory by moving tests to parent directory.xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16796 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-20Wrong bug identifier.xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16795 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-20Execute tests from the "bugs/closed" directory.xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16794 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-20Update test for bug 2846 in order to use "Fail".xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16793 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-20Use "Fail" rather than rely on exit code.xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16792 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-19Uminus.v : prepare this test file for the use of Failletouzey
- Highlight the fact that the line defining "up" is the one which should fail. - Factor code with stdlib's Hurkens.v - This way, this test could become a "shouldnotfail" test by placing two final "Fail" (before the definitions of "up" and "paradox"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16791 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-19universes-buraliforti-redef.v : repair a match after Pierre B. syntax changesletouzey
This file, which is currently expected to fail at the last line (with Universe Inconsistency), was actually failing earlier after Pierre Boutillier changed the patterns (parameters are required now). A final "Fail" will soon arrives here to avoid such issue in the future... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16790 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-19Prettyp: avoid useless "let module"letouzey
As hinted by X. Clerc, a "let module" induces some runtime cost, so let's try to avoid them when possible. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16789 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-19Made the filename of compiled files explicit, i.e. add a ./ prefixppedrot
whenever the filename was given alone. This caused strange behaviour of coqtop that was compiling stuff we didn't want to just because it was somewhere in its loadpath. This is why FingerTree was not compiling, btw, as it had two files equally named in two different paths. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16788 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-19Get rid of the uses of deprecated OCaml elements (still remaining compatible ↵xclerc
with OCaml 3.12.1). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16787 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-18At least made the evar type opaque! There are still 5 remaining unsafeppedrot
casts of ints to evars. - 2 in Evarutil and Goal which are really needed, even though the Goal one could (and should) be removed; - 2 in G_xml and Detyping that are there for completeness sake, but that might be made anomalies altogether; - 1 in Newring which is quite dubious at best, and should be fixed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16786 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-18Removing the last global evar generation in Term_dnet. The veryppedrot
fact that the previous implementation was working is still black magic to me, as evars may have collided in intriguing ways... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16785 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-18Removing unused code from Term_dnet.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16784 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-18Removing almost all new_untyped_evar, and a bunch of Evd.add.ppedrot
Ultimately all evars should be created with respect to a given evar map, instead of using a global counter. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16783 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-18Taming the simpl evar hack that used to use negative evars.ppedrot
Now we just generate evars in the given evar map. At least, the test-suite isn't broken... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16782 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-14Slightly more compact representation of 'a substituted type,ppedrot
removing an unneeded indirection. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16781 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-13When Coq is reset-initialed by CoqIDE, do reset jobs countersgareuselesinge
Coq is not going to send any feedback message for the brute-force canceled jobs, given that the process was killed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16780 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-13fix error reporting window size calculationgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16779 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 11:20:16 +0000