aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2011-04-15Documentation typo.gmelquio
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14008 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-14More informative anomaly.herbelin
Signed-off-by: Tom Prince <tom.prince@ualberta.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14002 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-14Add directories in COQPATH to search path.herbelin
This is to allow users to install plugins when coq is installed system-wide. Signed-off-by: Tom Prince <tom.prince@ualberta.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14001 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-14Reorder search path order, so the standard library is search last.herbelin
This allows the construction of an extended library that shadows the standard library. Signed-off-by: Tom Prince <tom.prince@ualberta.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14000 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-13Extraction: opaque terms are not traversed anymore by defaultletouzey
In signatures, opaque terms are always seen as parameters. In implementations, a flag Set/Unset Extraction AccessOpaque allows to customize things: - Set : opacity is ignored (this is the old behavior) - Unset : opaque terms are extracted as axioms (default now) Some warnings are anyway emitted when extraction encounters informative opaque terms. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13999 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-13Revert "Add [Polymorphic] flag for defs"msozeau
This reverts commit 33434695615806a85cec88452c93ea69ffc0e719. Conflicts: kernel/term_typing.ml test-suite/success/polymorphism.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13998 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-13Put dependent subgoals first so as to allow backtracking on them, might ↵msozeau
change resolution time quite a bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13997 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-13- Make typeclass transparency information directly availablemsozeau
- Fix pretyping to consider remaining unif problems with the right transparency information. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13996 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-13- Remove create_evar_defsmsozeau
- Be careful with consider_remaining_unif_problems: it might instantiate an evar, including the current goal! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13995 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-13Fix merge.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13994 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-13- Improve unification (beta-reduction, and same heuristic as evarconv for ↵msozeau
reducing matches). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13993 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-13Fix scripts relying on unification not doing any beta reduction.msozeau
They are actually simpler, sometimes using the [rewrite at] variant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13992 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-13Unify meta types with the right flags, add betaiotazeta reduction to ↵msozeau
unification (potentially harmful) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13991 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-13Proper typing of metavariables, type errors were completely ignored ↵msozeau
before... Use sort constraint checking as in evarconv as well git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13990 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-13- Do not make constants with an assigned type polymorphic (wrong unfoldings).msozeau
- Add Set Typeclasses Debug/Depth n options for typeclasses eauto. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13989 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-13Add [Polymorphic] flag for defsmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13988 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-12Subtyping: align coqtop behavior concerning opaque csts on coqchk's oneletouzey
After discussion with Bruno and Hugo, coqtop now accepts that an opaque constant in a module type could be implemented by anything of the right type, even if bodies differ. Said otherwise, with respect to subtyping, an opaque constant behaves just as a parameter. This was already the case in coqchk, and a footnote in documentation is advertising for quite some time that: "Opaque definitions are processed as assumptions." Truly, it might seem awkward that "Definition x:=3" can implement "Lemma x:nat. Proof 2. Qed." but the opacity ensures that nothing can go wrong afterwards, since Coq is forced to ignore that the x in signature has body "2". Similarly, "T with Definition x := c" is now legal when T contains an opaque x, even when this x isn't convertible with c. By avoiding accesses to opaque bodies, we also achieve some speedup (less delayed load of .vo final sections containing opaque terms). Nota: the extraction will have to be adapted, since for the moment it might access the body of opaque constants: the warning emitted when doing that should become an error. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13987 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-12remove old traces of SearchIsos (never ported to 7.x nor 8.x)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13986 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 10:19:21 +0000