aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coq.ml
Commit message (Collapse)AuthorAge
* Coqide: let's try to be synchronuous when killing coqtopGravatar letouzey2011-04-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14051 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqlib: avoid deadlock under win32 with force_reset_initialGravatar letouzey2011-04-21
| | | | | | | | | | | | The force_reset_initial starts by killing coqtop, then it tries to acquire the lock on coq_computing. If it works, no jobs are pending, we do the real reset_initial (launch of a new coqtop + removal of buffer coloring) ourself. Otherwise, the function do_if_not_computing is running, the death of coqtop will raise a RestartCoqtop exception there, triggering a reset_initial. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14049 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: back to using Unix.stderr in create_processGravatar letouzey2011-04-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14048 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: better handling of stdout/stderr in win32Gravatar letouzey2011-04-21
| | | | | | | | | | | | | | | | | | Now that coqide is a console-free win32 app, writing to nonexistent stdout/stderr lead to Sys_error. To avoid that: - We reroute coqide's stdout/stderr to either a pipe that will stay unread (by default), or to a temp log file (in debug mode). - When doing create_process, avoid referring to Unix.stderr: anything printed by coqtop to its stderr will be merged in the regular channel. - On the coqtop side, remove the awkward fix consisting in a \r printed on stderr apparently to fix coqide.byte. This fix is probably obsolete since the separation of coqide and coqtop as distinct processes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14047 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: quote coqtop filename if necessaryGravatar letouzey2011-04-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14045 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: a special kill function for win32Gravatar letouzey2011-04-21
| | | | | | | | | | | | This is implemented as a C external launching the TerminateProcess of the Win32 API. This should be considered as quite experimental (cf. the way we handle pid in the comment of ide_win32_stubs.c). I don't know how to emulate an interrupt (Ctrl-C), for now the two button "Restart" and "Interrupt" have the same semantics on win32 (kill the subprocess and start at top). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14044 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: try to avoid displaying error messages on coqide's consoleGravatar letouzey2011-04-21
| | | | | | | | | In Win32, these messages may trigger some Sys_error if we try to turn coqide into a true windows app (no console). To be continued... The best way would be probably to re-route the whole stdout and stderr to something else via dup2, but to what ? A log file ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14043 85f007b7-540e-0410-9357-904b9bb8a0f7
* Win32: if we make coqide console-free, then stderr/stdout/sdtin shouldn't be ↵Gravatar letouzey2011-04-21
| | | | | | | | | | | | | | | | | | | | | | used This is an adaptation of commit r13751 of branch 8.3 Even if coqide.exe keeps its console by default for the moment, we try to allow turning it off (for instance via the mkwinapp tool) : for that we need to be cautious about the use of functions like prerr_endline. Since stderr doesn't exists in this settings, such functions trigger a Sys_error "bad file descriptor". This patch protects many access to std** by a (try ... with _ ->()). Nota: with camlp5 < 6.02.1, Print Grammar was also generating such a Sys_error. TODO: we should try to figure a way of displaying messages (both debug and early/late error message). A log file ? A popup ? diplay in the response buffer ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14040 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: avoid confusion of process when restarting coqtop + cosmeticGravatar letouzey2011-03-30
| | | | | | | | | | | | | | | | | | | When using "Goto start" while many phrases are evaluated, it's frequent with earlier code that the restart occurs between two phrases, and hence the second is sent to the new coqtop, triggering things like "Anomaly: NoCurrentProof". To avoid that, Coq.coqtop is now immutable (no silent switch of channels). In Coqide, toplvl and mycoqtop are now references, that are updated when using reset_coqtop. We organize things in order to have only one access to mycoqtop during code that does many sequential calls to coqtop. This way, when coqtop changes, the code speaks to the old one, and gets some exception when writing/reading on a close channel. By the way, some documentation, cleanup, etc etc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13942 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ide_slave: better handling of Ctrl-CGravatar letouzey2011-03-30
| | | | | | | | | - During input and output to coqide, we postpone Ctrl-C instead of ignoring them. For that we use Util.interrupt and Util.check_for_interrupt. - During evaluation of coqide requests, a Ctrl-C directly raises Sys.break, which is more reliable than waiting for the next Util.check_for_interrupt git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13939 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ide: misc (nicer message than End_of_file, a useless try removedGravatar letouzey2011-03-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13935 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ide: new option -coqtop <mycoqtop> + remove wrong quoting of argsGravatar letouzey2011-03-28
| | | | | | | | | | | | | * Run "coqide -coqtop someothercoqtop" if you want to use a toplevel which isn't the one coming alongside coqide. To be documented, to be improved (maybe an field in coqide's preferences ?). coqide -h should display this kind of ide-specific option. * Since we now use create_process instead of open_process, we don't use /bin/sh, hence running Filename.quote on args was actually wrong. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13932 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ide: more reorganisation and cleanupGravatar letouzey2011-03-25
| | | | | | | | | | | | | | | | | | | - Avoid using Util which depends on Compat and hence Camlp4 - Instead, a small Minilib module specific to coqide, which duplicate 5 functions from Util (50 lines) - some dead code removal - the coqlib variable is asked to coqtop - remove obsolete Util.check_for_interrupt This way, coqide only depends on 3 files outside ide/ : Coq_config, Flags, Ide_intf. Makefile and ocamlbuild are adapted accordingly. TODO: how should we signal coqide error, warnings, etc ? For the moment, some Printf.eprintf, some failwith. To uniformize later... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13930 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ide_intf : change type of location in ideGravatar letouzey2011-03-25
| | | | | | | We use (int * int) option instead of Loc.t, it's easier to use later in coqide, and this way we do not depend on camlp4,5 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13929 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ide: stronger separation from coqtopGravatar letouzey2011-03-23
| | | | | | | | | | | | | | | Former module Ide_blob is now divided in Ide_intf (linked both by coqtop and coqide) and Ide_slave (now only in coqtop). Ide_intf has almost no dependencies, we can now compile coqide with only coq_config.cm* and lib.cm(x)a TODO: - Devise a better way to display whether coqide is byte or opt in the about message (instead of Mltop.is_native, I display now the executable name, which hopefully contains opt or byte) - Check the late error handling in ide/coq.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13927 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ide: experimentally allow coqide to interrupt or kill coqtopGravatar letouzey2011-03-23
| | | | | | | | | | | | | | | | | | | | | | | - We now use create_process instead of open_process, and stores the answered pid. - The "Stop" button now sends a Sigint signal to this coqtop pid. - The "Goto Start" button now works even if a computation is ongoing, a new process is spawned and the previous one is killed -9, and then a waitpid is done to avoid having zombies around. Note that currently a vm_compute won't be stopped by a "Stop", but only by a "Goto Start". This can be quite confusing. How to properly document that "Goto Start" has the side effect of being a kill ? Maybe we could check someday if the Ctrl-C has been successful, and kill -9 if not ? Or maybe make coqide aware of a flag "we_are_vm_computing" and then kill -9 instead of Ctrl-C in this case ? TODO: - for the moment a forced "Goto Start" displays an unfriendly anomaly - check if all this works under Windows (probably but not sure). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13926 85f007b7-540e-0410-9357-904b9bb8a0f7
* Call coqtop with -nois when probing for filesGravatar pboutill2011-01-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13775 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reverted r13715 "Add improved indenters that rely on the current proof state ↵Gravatar gmelquio2011-01-06
| | | | | | | | to choose the indentation depth." It seems to be the cause for bug #2472. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13766 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove Safe_marshalGravatar glondu2011-01-06
| | | | | | | | | | | | Safe_marshal was using intermediate strings that are subject to Sys.max_string_length limitation. Use directly binary channel-oriented functions instead. This is a fix for bug #2471. Remark: this might reduce robustness w.r.t. noise in the communication channel. AFAIK, the original purpose of Safe_marshal was to work around a bug on Windows... this should be investigated further. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13765 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add improved indenters that rely on the current proof state to choose the ↵Gravatar gmelquio2010-12-14
| | | | | | | | | | indentation depth. Patch by Cedric Auger. These two indenters need to be exercised a bit to see if they are actually useful to users. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13715 85f007b7-540e-0410-9357-904b9bb8a0f7
* Made new comm. model between coq and coqide support '-R foo ""'-style option.Gravatar herbelin2010-12-04
| | | | | | This fixes bug #2442. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13683 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improved error messages in CoqIDE:Gravatar herbelin2010-11-07
| | | | | | | | | | | - add a check that coqtop can be run before starting the interface - returns the error message in case of problem - made illegal option message more informative - use coqtop.byte when coqide.byte (is it a good heuristic?) - made debugging messages silent by default in ide/undo.ml (Ctrl-C was calling Pervasives.prerr_endline instead of Ideutils.prerr_endline) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13627 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE argv parsing delegated to coqtopGravatar vgross2010-09-14
| | | | | | | | | | Introduces some hacks to have a consistent user experience. When coqtop prints info on self then exit, return code is 2 if called with -filteropts, 0 else For now, no options are accepted by coqide. there is no way for now to specify a filename that begins with a dash. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13415 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqide: s/Sys.argv.(0)/Sys.executable_name/ for coqtop (cf #2341)Gravatar glondu2010-07-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13277 85f007b7-540e-0410-9357-904b9bb8a0f7
* Robustness fix : clean restart of coqtop on pipe error + force matchingGravatar vgross2010-07-05
| | | | | | of coqtop return codes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13245 85f007b7-540e-0410-9357-904b9bb8a0f7
* Stronger checks on coqtop termination, warning when zombies.Gravatar vgross2010-07-05
| | | | | | Also, reindentation + typed_notebook simplification git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13241 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing tabs closing problems by removing activation infrastructure.Gravatar vgross2010-07-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13238 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixing error message display.Gravatar vgross2010-06-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13082 85f007b7-540e-0410-9357-904b9bb8a0f7
* added -args option to coqide to pass options to coqtopsGravatar vgross2010-06-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13046 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE goes multiprocessGravatar vgross2010-05-31
| | | | | | | | | | | | | | | This commit changes many things in CoqIDE, and several breakage are to be expected. So far, evaluation in standard tactic mode and backtracking seems to be working. Future work : - clean up the thread management crud remaining in ide/coqide.ml - rework the exception handling - rework the init system in Coqtop plus many other things git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13043 85f007b7-540e-0410-9357-904b9bb8a0f7
* More indirection.Gravatar vgross2010-05-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13042 85f007b7-540e-0410-9357-904b9bb8a0f7
* Introducing strong typing for IDE - toplevel IPCGravatar vgross2010-05-31
| | | | | | Obj.magic in toplevel/ide_blob.ml is the only way to simulate GADT. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13041 85f007b7-540e-0410-9357-904b9bb8a0f7
* deporting Coq specific code from ide to toplevel.Gravatar vgross2010-05-31
| | | | | | Still messy. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13040 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modifying startup sequenceGravatar vgross2010-05-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13039 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add (almost) compatibility with camlp4, without breaking support for camlp5Gravatar letouzey2010-05-19
| | | | | | | | | | | | | | | | | | | | | | | The choice between camlp4/5 is done during configure with flags -usecamlp5 (default for the moment) vs. -usecamlp4. Currently, to have a full camlp4 compatibility, you need to change all "EXTEND" and "GEXTEND Gram" into "EXTEND Gram", and change "EOI" into "`EOI" in grammar entries. I've a sed script that does that (actually the converse), but I prefer to re-think it and check a few things before branching this sed into the build mechanism. lib/compat.ml4 is heavily used to hide incompatibilities between camlp4/5 and try to propose a common interface (cf LexerSig / GrammarSig). A few incompatible quotations have been turned into underlying code manually, in order to make the IFDEF CAMLP5 THEN ... ELSE ... END parsable by both camlp4 and 5. See in particular the fate of <:str_item< declare ... end >> Stdpp isn't used anymore, but rather Ploc (hidden behind local module Loc). This forces to use camlp5 > 5.01. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13019 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #2315 : printing of defined evars in Coqide.Gravatar aspiwack2010-05-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13003 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pfedit.resume_proof doesn't implicitly Pfedit.suspend_proofGravatar pboutill2010-05-05
| | | | | | | | | | | - ide doesn't crash anymore at any backtrack - I don't see if vernacentries.ml did the same assumption so I didn't change anything. (The only other use of resume_proof) - ide still raises "NoCurrentProof" when you type a bad keyword such as "Priint"... But at least, this on is catch somewhere ! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12993 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fail: a way to check that a command is refused without blocking a scriptGravatar letouzey2010-04-30
| | | | | | | | | | | | | | | | | | | | | | | "Fail cmd" is similar to "Time cmd", but instead of printing the execution time, it reverse the exit status of cmd. "Fail cmd" is successful iff cmd has ended with an error. This was, we can demonstrate erroneous commands in a script for pedagogical or testing purpose without having to comment it in order to play the rest of the script in coqide/PG. Coq < Fail Foo. The command has indeed failed with message: => Error: Unknown command of the non proof-editing mode. Coq < Fail Check Prop. Prop : Type Error: The command has not failed ! Two more remarks: - Fail doesn't catch anomalies. - Yes it it possible to write things like Fail Fail ... :-) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12981 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
| | | | | | | | | | | - Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a fairly large commit (around 140 files and 7000 lines of code impacted), it will cause some troubles for sure (I've listed the know regressions below, there is bound to be more). At this state of developpement it brings few features to the user, as the old tactics were ported with no change. Changes are on the side of the developer mostly. Here comes a list of the major changes. I will stay brief, but the code is hopefully well documented so that it is reasonably easy to infer the details from it. Feature developer-side: * Primitives for a "real" refine tactic (generating a goal for each evar). * Abstract type of tactics, goals and proofs * Tactics can act on several goals (formally all the focused goals). An interesting consequence of this is that the tactical (. ; [ . | ... ]) can be separated in two tacticals (. ; .) and ( [ . | ... ] ) (although there is a conflict for this particular syntax). We can also imagine a tactic to reorder the goals. * Possibility for a tactic to pass a value to following tactics (a typical example is an intro function which tells the following tactics which name it introduced). * backtracking primitives for tactics (it is now possible to implement a tactical '+' with (a+b);c equivalent to (a;c+b;c) (itself equivalent to (a;c||b;c)). This is a valuable tool to implement tactics like "auto" without nowing of the implementation of tactics. * A notion of proof modes, which allows to dynamically change the parser for tactics. It is controlled at user level with the keywords Set Default Proof Mode (this is the proof mode which is loaded at the start of each proof) and Proof Mode (switches the proof mode of the current proof) to control them. * A new primitive Evd.fold_undefined which operates like an Evd.fold, except it only goes through the evars whose body is Evar_empty. This is a common operation throughout the code, some of the fold-and-test-if-empty occurences have been replaced by fold_undefined. For now, it is only implemented as a fold-and-test, but we expect to have some optimisations coming some day, as there can be a lot of evars in an evar_map with this new implementation (I've observed a couple of thousands), whereas there are rarely more than a dozen undefined ones. Folding being a linear operation, this might result in a significant speed-up. * The declarative mode has been moved into the plugins. This is made possible by the proof mode feature. I tried to document it so that it can serve as a tutorial for a tactic mode plugin. Features user-side: * Unfocus does not go back to the root of the proof if several Focus-s have been performed. It only goes back to the point where it was last focused. * experimental (non-documented) support of keywords BeginSubproof/EndSubproof: BeginSubproof focuses on first goal, one can unfocus only with EndSubproof, and only if the proof is completed for that goal. * experimental (non-documented) support for bullets ('+', '-' and '*') they act as hierarchical BeginSubproof/EndSubproof: First time one uses '+' (for instance) it focuses on first goal, when the subproof is completed, one can use '+' again which unfocuses and focuses on next first goal. Meanwhile, one cas use '*' (for instance) to focus more deeply. Known regressions: * The xml plugin had some functions related to proof trees. As the structure of proof changed significantly, they do not work anymore. * I do not know how to implement info or show script in this new engine. Actually I don't even know what they were suppose to actually mean in earlier versions either. I wager they would require some calm thinking before going back to work. * Declarative mode not entirely working (in particular proofs by induction need to be restored). * A bug in the inversion tactic (observed in some contributions) * A bug in Program (observed in some contributions) * Minor change in the 'old' type of tactics causing some contributions to fail. * Compilation time takes about 10-15% longer for unknown reasons (I suspect it might be linked to the fact that I don't perform any reduction at QED-s, and also to some linear operations on evar_map-s (see Evd.fold_undefined above)). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12961 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changing types to reflect futur separation between toplevel and ide.Gravatar vgross2010-03-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12880 85f007b7-540e-0410-9357-904b9bb8a0f7
* Goal generation deported into ide/coq.ml, single function to obtainGravatar vgross2010-03-23
| | | | | | all current goals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12878 85f007b7-540e-0410-9357-904b9bb8a0f7
* New functions for goals fetching.Gravatar vgross2010-03-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12877 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug in backtracking.Gravatar vgross2010-03-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12876 85f007b7-540e-0410-9357-904b9bb8a0f7
* debuggingGravatar vgross2010-03-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12875 85f007b7-540e-0410-9357-904b9bb8a0f7
* New backtracking code + fix bug #2082.Gravatar vgross2010-02-26
| | | | | | Previous code checkings were too lax, and information was lost. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12823 85f007b7-540e-0410-9357-904b9bb8a0f7
* Introducing a dual stack setupGravatar vgross2010-02-26
| | | | | | | The first stack lives in coqide and tracks the tagging and locking, the second lives in coq and tracks the commands. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12822 85f007b7-540e-0410-9357-904b9bb8a0f7
* New API for backtracking.Gravatar vgross2010-02-26
| | | | | | | Aside the command stack, the only parameter is the number of step to go back. Went back and forth without sync losses on tests-suite/ide/undo.v. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12821 85f007b7-540e-0410-9357-904b9bb8a0f7
* Redispatch of printing tweaking hooks.Gravatar vgross2010-02-26
| | | | | | | We want to tweak the printing options when we want to display the results, not when we are evaluating vernac. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12820 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 10:36:31 +0000