aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2011-04-11Catch NotArity exception and transform it into an anomaly in retyping.msozeau
Add a temporary fix in solve_simple_eqn to catch anomalies coming from retyping because the unification algorithm with metas doesn't respect the precondition that evar instances should be well-typed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13985 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-08ocamlbuild: support again camlp5 in addition to camlp4letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13984 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-08Applying Tom Prince's patch to coqdep not correctly applying the -R visibilityherbelin
discipline to files from stdlib or user library (also factorized code with add_known) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13982 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-08A kind of reply to bug 2444pboutill
coq_makefile uses ocaml{c,opt}.opt if it uses coqc -opt and ocaml‘c,opt} if it uses coqc -byte. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13980 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-08weak dependency of coqtop for coqide and coqc (bug 2390)pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13979 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-08A module out of Program to have list notations (bug 2463)pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13978 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-08@ in index of refman (last request of bug 2494)pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13977 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-08Add "make full-stdlib" to make all the doc in pdf as ask by bug 2395pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13976 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-08More up to date About in coqidepboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13975 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-08Macos integration step2 : shutdownpboutill
You can quit coqide from the dock and reboot/shutdown will ask you if you want to save your unsavec files. Asks for a re"configure". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13974 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-08coqide shutdown process change (and out the main function)pboutill
It now checks for 5 sec every 0.1 sec if is there is still running coqtop then it asks the user if he wants to leave zombies or cancel quit. (Cancel quit was continue to wait). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13973 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-08Applying Tom Prince's patch for build_constant_by_tactic not able toherbelin
use a lemma name chosen by the caller (here tclABSTRACT) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13972 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-08Made warning about ending comments in string less intrusive so as to supportherbelin
things like (* "forall X : (* Type *), X" *) without warnings git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13971 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-08Applying and reworking Tom Prince's patch for test-suite/failure/universes2.vherbelin
which did not test what it was supposed to test git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13970 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-08Replaced printing number of ill-typed branch by printing name of constructorherbelin
when a "match" is kernel-ill-typed (probably rarely visible from end user anyway but useful for debugging) + dead code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13969 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-08Fixed "Eval ... in t" when t has still metavariables.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13968 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-08Fixing multiple printing bugs with "Notation f x := ..."herbelin
- Missing space and bad constr level in "About f" - Display of arguments missing when used as a pattern notation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13966 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-07Extraction: unfolds the let-in created by Program when handling "match"letouzey
This leads to code closer to the original input of the user, and moreover some more dummy __ may be removed this way. To avoid unfolding by mistake user's variables, we change the name of these generated let-in into "program_branch_NN" instead of "branch_NN" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13964 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-07Extraction: avoid some useless Obj.magic by fixing my ML type unifierletouzey
Due to wrong pattern order in Mlutil.mgu, simple situations like ?n == ?n were considered unsolvable as soon as one side was aliased (i.e. inside an instantiated type meta). Moreover, use general equality as last resort, instead of forgetting cases like Taxiom == Taxiom. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13963 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-06Fixing bug #2475 (ability to use binders in the syntax of fields was not in doc)herbelin
(backport from 8.3) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13961 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-06A few extra combinators about rel_declaration/named_declaration + a bit of docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13959 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-06Fix dev/base_include after change of constant_bodyletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13958 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-06Fixes the weird bug of the declarative proof mode (Czar) both in emacs and coqc.aspiwack
Patch submitted by Tom Prince. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13957 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-06Add 'Existing Instances' declaration to declare multiple instances at once.letouzey
This is useful, for example, in declaring the projection of the dependent record bundled form of an unbundled typeclass. Patch submitted by Tom Prince git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13956 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-03Update documentation concerning proofs loading (cf last commit)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13954 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-03Fix last commit about coqdep: not everyone has a user-contrib dirletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13953 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-03Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksletouzey
The recent experiment with -dont-load-proofs in the stdlib showed that this options isn't fully safe: some axioms were generated (Include ? functor application ? This is still to be fully understood). Instead, I've implemented an idea of Yann: only load opaque proofs when we need them. This is almost as fast as -dont-load-proofs (on the stdlib, we're now 15% faster than before instead of 20% faster with -dont-load-proofs), but fully compatible with Coq standard behavior. Technically, the const_body field of Declarations.constant_body now regroup const_body + const_opaque + const_inline in a ternary type. It is now either: - Undef : an axiom or parameter, with an inline info - Def : a transparent definition, with a constr_substituted - OpaqueDef : an opaque definition, with a lazy constr_substitued Accessing the lazy constr of an OpaqueDef might trigger the read on disk of the final section of a .vo, where opaque proofs are located. Some functions (body_of_constant, is_opaque, constant_has_body) emulate the behavior of the old fields. The rest of Coq (including the checker) has been adapted accordingly, either via direct access to the new const_body or via these new functions. Many places look nicer now (ok, subjective notion). There are now three options: -lazy-load-proofs (default), -force-load-proofs (earlier semantics), -dont-load-proofs. Note that -outputstate now implies -force-load-proofs (otherwise the marshaling fails on some delayed lazy). On the way, I fixed what looked like a bug : a module type (T with Definition x := c) was accepted even when x in T was opaque. I also tried to clarify Subtyping.check_constant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13952 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-03Quickly avoid global axioms in Loic new files about ringletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13951 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-01Adjust coqdep so that it behaves like coqtop with respect to the ↵gmelquio
user-contrib directory. In particular, this directory should be traversed recursively and the full name of its libraries should not be prefixed by the "Coq" logical path. This fixes coqdep spamming the following message while the yyy library is in the user-contrib loadpath. *** Warning: in file xxx.v, library yyy.v is required and has not been found in loadpath! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13949 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-01CHANGES: a word about recent changes in coqide, about Ctrl-C in vmletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13948 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-01Checks for signals in VM, allowing it to be interrupted by Ctrl-C (experimental)letouzey
We simply reuse the ocaml flag caml_signals_are_pending and the function caml_process_pending_signals, and place a test at some place of the interpreter loop (at a similar location as in ocaml byterun/interp.c). The symbols caml_* we use are not officially made public in *.h installed alongside ocaml, but they seem pretty stable (there since at least ocaml 3.10, independent of arch and of byte/asm), so we access them via "extern". For once, thanks dirty C... In addition to that, when catching a Ctrl-C, we reset the vm via "coq_sp = coq_stack_high" as suggested by Benjamin G. This patch should be quite portable, it might even work in win32. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13947 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-31Did that adding a rule for printing applications as "f(x)" works.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13946 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-31As remarked by Enrico, we'd better use eq_constr than structural equalityherbelin
(it is a priori optimized but also able to reason modulo equality of names and modulo alpha-conversion). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13945 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-31Extraction: customized inductives are always standardglondu
If the user customized the inductive, he should know what he is doing... This (hopefully) fixes bug #2482. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13944 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-30Cyclic: a small optimisation with nice effect on BigN.mul (thinks Benjamin)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13943 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-30Coqide: avoid confusion of process when restarting coqtop + cosmeticletouzey
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
2011-03-30Ide_intf: documentation of calls + debug printing of calls/answersletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13941 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-30Ide_intf: remove useless int answer to the "interp" and "rewind" callsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13940 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-30Ide_slave: better handling of Ctrl-Cletouzey
- 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
2011-03-30Coqide: synchronise the reset_initial via the coq_computing mutexletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13938 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-28Ide_slave : fix last commit, use ad_hoc catch_break instead of Sys.catch_breakletouzey
Default behavior for (Sys.catch_break false) is to exit, while we want the opposite: survive. When I write an ad-hoc catch_break, I'd better use it, damnit ! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13937 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-28Ide: restaure compilation of ide/macjokes.c removed by mistakeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13936 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-28Ide: misc (nicer message than End_of_file, a useless try removedletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13935 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-28Ide_slave: improved handling of exceptions (in particular ^C)letouzey
we try to ignore ^C during I/O but enable it during treatment of requests. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13934 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-28Ide_slave: a more robust current_status () functionletouzey
- Due to -top foobar, or -notop, the current dir_path () doesn't necessary starts by Top. - Start documenting Ide_intf git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13933 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 16:42:10 +0000