aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* STM: some refactoring, support revised CoqIDE protocolGravatar gareuselesinge2013-09-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16815 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE ported to the revides protocolGravatar gareuselesinge2013-09-30
| | | | | | | | | | | - 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
* fake_ide ported to the new protocol (FIXME tests fail)Gravatar gareuselesinge2013-09-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16813 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE protocol/serialization revisedGravatar gareuselesinge2013-09-30
| | | | | | | | | | | | - 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
* lib/cstack: various improvementsGravatar gareuselesinge2013-09-30
| | | | | | | - 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
* lib/vcs: various improvementsGravatar gareuselesinge2013-09-30
| | | | | | | | - 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
* lib/dag: various improvementsGravatar gareuselesinge2013-09-30
| | | | | | | - 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
* lib/future: computations that are Exn can be replacedGravatar gareuselesinge2013-09-30
| | | | | | | | 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
* Made rewrite tactic strategies pure. They were using quite uglilyGravatar ppedrot2013-09-28
| | | | | | 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
* Removing a bunch of generic equalities.Gravatar ppedrot2013-09-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16806 85f007b7-540e-0410-9357-904b9bb8a0f7
* Opacifying the type of strategies.Gravatar ppedrot2013-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16805 85f007b7-540e-0410-9357-904b9bb8a0f7
* Splitting Rewrite into a code part and a CAMLP4-dependent one.Gravatar ppedrot2013-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16804 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing useless evar-related stuff.Gravatar ppedrot2013-09-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16803 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding evar printing to debugger.Gravatar ppedrot2013-09-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16802 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing ocamldebug compilation by adding thread linking.Gravatar ppedrot2013-09-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16801 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix name clash in "failure/inductive.v".Gravatar xclerc2013-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16800 85f007b7-540e-0410-9357-904b9bb8a0f7
* Merge "circular_subtyping?.v" tests into a single "circular_subtyping.v" test.Gravatar xclerc2013-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16799 85f007b7-540e-0410-9357-904b9bb8a0f7
* Merge "inductive?.v" tests into a single "inductive.v" test.Gravatar xclerc2013-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16798 85f007b7-540e-0410-9357-904b9bb8a0f7
* Get rid of "shouldsucceed" subdirectory by moving tests to parent directory.Gravatar xclerc2013-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16797 85f007b7-540e-0410-9357-904b9bb8a0f7
* Get rid of "shouldfail" subdirectory by moving tests to parent directory.Gravatar xclerc2013-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16796 85f007b7-540e-0410-9357-904b9bb8a0f7
* Wrong bug identifier.Gravatar xclerc2013-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16795 85f007b7-540e-0410-9357-904b9bb8a0f7
* Execute tests from the "bugs/closed" directory.Gravatar xclerc2013-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16794 85f007b7-540e-0410-9357-904b9bb8a0f7
* Update test for bug 2846 in order to use "Fail".Gravatar xclerc2013-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16793 85f007b7-540e-0410-9357-904b9bb8a0f7
* Use "Fail" rather than rely on exit code.Gravatar xclerc2013-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16792 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uminus.v : prepare this test file for the use of FailGravatar letouzey2013-09-19
| | | | | | | | | | - 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
* universes-buraliforti-redef.v : repair a match after Pierre B. syntax changesGravatar letouzey2013-09-19
| | | | | | | | | | 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
* Prettyp: avoid useless "let module"Gravatar letouzey2013-09-19
| | | | | | | 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
* Made the filename of compiled files explicit, i.e. add a ./ prefixGravatar ppedrot2013-09-19
| | | | | | | | | | | 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
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ↵Gravatar xclerc2013-09-19
| | | | | | with OCaml 3.12.1). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16787 85f007b7-540e-0410-9357-904b9bb8a0f7
* At least made the evar type opaque! There are still 5 remaining unsafeGravatar ppedrot2013-09-18
| | | | | | | | | | | | 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
* Removing the last global evar generation in Term_dnet. The veryGravatar ppedrot2013-09-18
| | | | | | | 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
* Removing unused code from Term_dnet.Gravatar ppedrot2013-09-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16784 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing almost all new_untyped_evar, and a bunch of Evd.add.Gravatar ppedrot2013-09-18
| | | | | | | 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
* Taming the simpl evar hack that used to use negative evars.Gravatar ppedrot2013-09-18
| | | | | | | | 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
* Slightly more compact representation of 'a substituted type,Gravatar ppedrot2013-09-14
| | | | | | removing an unneeded indirection. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16781 85f007b7-540e-0410-9357-904b9bb8a0f7
* When Coq is reset-initialed by CoqIDE, do reset jobs countersGravatar gareuselesinge2013-09-13
| | | | | | | 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
* fix error reporting window size calculationGravatar gareuselesinge2013-09-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16779 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE: new async error reporting window and slaves statusGravatar gareuselesinge2013-09-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16778 85f007b7-540e-0410-9357-904b9bb8a0f7
* STM pretty printer should never failGravatar gareuselesinge2013-09-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16777 85f007b7-540e-0410-9357-904b9bb8a0f7
* fix STM feeback on running jobsGravatar gareuselesinge2013-09-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16776 85f007b7-540e-0410-9357-904b9bb8a0f7
* Do no compage wg_Notebook terms with (=)Gravatar gareuselesinge2013-09-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16775 85f007b7-540e-0410-9357-904b9bb8a0f7
* Unplugging Autoinstance. The code is still here if someone wishesGravatar ppedrot2013-09-12
| | | | | | to fix it, but it should be eventually erased. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16774 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE: show number of proofs being checked in backgroundGravatar gareuselesinge2013-09-12
| | | | | | good test: Nijmegen/QArithSternBrocot/Zaux.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16773 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minimal implementation of `Shallow marshalling of LibGravatar gareuselesinge2013-09-12
| | | | | | Just sufficient to make abstract work in such an (empty) lib. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16772 85f007b7-540e-0410-9357-904b9bb8a0f7
* Unknown commands starting a proof were not setting the proof mode.Gravatar gareuselesinge2013-09-12
| | | | | | Fixes Orsay/Containers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16771 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove outdated commentGravatar gareuselesinge2013-09-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16770 85f007b7-540e-0410-9357-904b9bb8a0f7
* VernacList handling was lost in STM mergeGravatar gareuselesinge2013-09-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16769 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug in CStack introduced by refactoringGravatar gareuselesinge2013-09-12
| | | | | | Refactorings should be tested, right? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16768 85f007b7-540e-0410-9357-904b9bb8a0f7
* Temporary fix of emacs mode for ProofGeneralGravatar letouzey2013-09-10
| | | | | | | | | | To the best of my knowledge, even with the latest cvs version of PG: - the goals must be finally displayed at each step - the <info>...</info> async feedback messages aren't handled yet. I'll check with Enrico what he intended with these two lines, but meanwhile let's comment them... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16767 85f007b7-540e-0410-9357-904b9bb8a0f7
* Change syntax of Hint Resolve to actually accept user-given priorities.Gravatar msozeau2013-09-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16766 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 06:17:05 +0000