aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2011-04-28coqtop -config returns coq returns coq environments at exection timepboutill
It looks like a variables definition part of a Makefile. Names are from coq makefiles. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14080 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-28Revert r14078 "Partial backtrack on the support for open terms in ↵gmelquio
destruct/induction:" While this is needed for supporting destruct with typeclasses on 8.4, it was not my intent to commit it yet (as a better fix might be in the work), so reverting it for now. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14079 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-28Partial backtrack on the support for open terms in destruct/induction:gmelquio
use type classes to possibly solve evars before trying to unify the term (or the dependencies of its type) agains a subterm of the current goal. This solves compatibility bug #2222. Mixing unification and type classes is left for future work. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14078 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-28Coqide: try to properly send interrupts to coqtop on Win32letouzey
We use GenerateConsoleCtrlEvent(CTRL_C_EVENT,...) after having attached coqide to the console of the coqtop we want to interrupt. Two caveats: - This code isn't compatible with Windows < XP SP1. - It relies on the fact that coqide is now a true GUI app, without console by default. If for some reason the console of coqide is restored (for instance via mkwinapp -unset), strange behavior of the interrupt button is to be expected, at the very least all instances of coqtop will get Ctrl-C instead of a precise one. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14077 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-28Adding "Tactic Notation" in doc index.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14076 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-28Fixing an "apply -> ... in hyp" bug (the hyp was considered as a fixedherbelin
ident by Ltac). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14074 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-28Fixed notation printing bug when curly brackets are involved (requestsherbelin
for adding spaces were not taken into account in notations containing patterns of the form "{ ident symbol", paradoxically resulting in adding extra spaces, e.g. when printing the type "{ x | P x }" of "exist", due to interferences with the heuristic for adding breaking points in Metasyntax.make_hunk). Also adapted output of test InitSyntax.v after commit r14018 improved the printing of "ex P" and "sig P". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14073 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-27Updating CHANGESherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14072 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-27Fixing output of Notations2.v test messed up in r14060herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14071 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-26Pcoq.ml4: fix a typo in a comment to please ocamldocletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14070 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-26G_vernac can be parsed without grammar.cmaletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14069 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-26dev/base_include: no more mod_self_idletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14068 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-26Fixing commit r14061 (changes in file tactics.ml were mistakenly committed).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14067 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-26Coqide: fix remove_current_view_page (#2499)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14065 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-25Fix for handling of -R "" in coqdoc (bug #2423).herbelin
(submitted by Tom Prince <tom.prince@ualberta.net>) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14063 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-25Fixing and completing interpretation of let's in notations for iterated binders.herbelin
(backport from trunk) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14061 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-25Fixing and completing interpretation of let's in notations for iterated binders.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14060 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-24Yet another bug in printing fix with let-in bindersherbelin
(backport from branch v8.3) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14058 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-24Fixing bug in printing let-in binders in fix/cofixherbelin
(backport from branch v8.3) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14055 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-24Fixed a bug of destruct which was sometimes forgetting local definitions ↵herbelin
behind it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14053 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-22Coqide: fix synchro when restarting during a single stepletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14052 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-21Coqide: let's try to be synchronuous when killing coqtopletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14051 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-21Coqide: remove some dead codeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14050 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-21Coqlib: avoid deadlock under win32 with force_reset_initialletouzey
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
2011-04-21Coqide: back to using Unix.stderr in create_processletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14048 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-21Coqide: better handling of stdout/stderr in win32letouzey
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
2011-04-21Coqide: typoletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14046 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-21Coqide: quote coqtop filename if necessaryletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14045 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-21Coqide: a special kill function for win32letouzey
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
2011-04-21Coqide: try to avoid displaying error messages on coqide's consoleletouzey
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
2011-04-21Coqide: better construction of default coqtop pathletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14042 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-21Win32: remove the need for Coq.bat and Coqide.batletouzey
This is an adaptation of commit r13750 of branch 8.3 - coqlib is currently computed relatively of Sys.executable_name, hence no need to set it manually - in Win32, better detection of user home dir : in System.ml, if HOME isn't set, we look now for HOMEDRIVE\HOMEPATH, and then for USERPROFILE - concerning PATH, in Win32 we now add coqbin (or the location of coqide) to PATH during the initialization. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14041 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-21Win32: if we make coqide console-free, then stderr/stdout/sdtin shouldn't be ↵letouzey
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
2011-04-21Ocamlbuild: in win32, coqide is now a console-free app by defaultletouzey
This is an adaptation of commit 13748 in 8.3 branch Making coqide console-free can be done via a link flag given to mingw. In case of problem with this setting, I also include a script mkwinapp.ml borrowed from project OCaml-Win32 (and slightly modified to allow restoring the console as well as removing it). Use: "mkwinapp coqide.exe" to make it console-free. "mkwinapp -unset coqide.exe" to go back to usual console app. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14039 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-21Win32: let's directly make coqtop.exe and coqide.exe incorporate coq.icoletouzey
This is an adaptation of commit 13747 for 8.3 branch git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14038 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-21bug fix: concurrent access of persistent_cachefbesson
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14037 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-20Coqide: Fix the command separator for external cmds (#2363)letouzey
We use "&&" instead of ";" which is - compatible with unix and win32 - more adequate anyway than ";" : no need to run the command if the cd has failed... Concerning coqdoc, since previous commit it should not be mandatory to provide the "--coqlib-path" option. We remove them... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14036 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-20Coqdoc: also try coqlib relative to the coqdoc binary locationletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14035 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-20Allow betaiota when checking unification of the types of metas (fixes ATBR ↵msozeau
contrib). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14032 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-20Don't force progress on instance applications, there is always progress when ↵msozeau
refining dependent instances git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14031 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-20This is used in the rippling plugin. This also allows fixing bug #2188.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14030 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-19Declarative mode: fix escape and return.aspiwack
The declarative mode should now work almost like in v8.3 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14029 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-19Fix thumb2-related build errorglondu
Bug-Debian: http://bugs.debian.org/cgi-bin/bugreport.cgi?bug=622882 Signed-off-by: Konstantinos Margaritis <markos@genesi-usa.com> Signed-off-by: Stephane Glondu <steph@glondu.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14027 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-18Fix generated script for NMake, a rewrite necessitates full conversion formsozeau
checking types. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14023 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-18Add a flag to control betaiota reduction during unification to maintain ↵msozeau
backward compatibility. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14022 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-16Fix unification of types of metavariables and error message for sort ↵msozeau
unification. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14020 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-15Take benefit of eta-expansion so that "ex P" is displayed "exists x, P x".herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14018 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-15Coqc: fix the exit codeletouzey
Patch suggested by Benjamin Monate git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14016 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-15Extraction: nicer error when a toplevel module has no body (#2525)letouzey
I thought this situation wasn't possible, hence the Option.get. But it's apparently legal to use Declare Module anywhere, even outside a Module Type. No idea on how to handle that at extraction for the moment, hence a proper "unsupported" error message. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14013 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-15Extraction: allow extracting Ascii.ascii to native Char in Haskell (fix #2515)letouzey
We simply factorize code that was already existing for Ocaml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14011 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 21:53:31 +0000