aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2011-10-10Added information about evar origin in pretty-printing evd for debugherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14535 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-10Passed conv_algo to evar_define and move call to solve_refl toherbelin
evar_define so that it can recursively deal with evar/evar problems. Also, check_evar_instance now called after each instantiation. Also did a bit of file reformatting. The commit apparently induces a loss of some 0,4% on the compilation of the standard library. Maybe, introducing a heuristic to decide when to call check_evar_instance (which I guess is responsible for the overhead) might be a good thing to look at? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14534 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-10Proper fix for complement/flip instances.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14533 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-09mainbiblio.bib : get rid of merge marker from failed mergeletouzey
Thanks to Tom Prince for spotting this git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14530 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-08Scheme names: Use unprobable names + ensure names do not hide existing namesherbelin
when schemes are generated for internal use of Coq. Ideally, I would like to add these names asynchronously in name spaces relevant for the corresponding inductive type, what modules do not support since modules cannot be reopened. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14529 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-08Rely on kernel to know if a name is already used so as to be consistent with it.herbelin
Maybe could we keep only the kernel check, but message would certainly need to be reformulated then. For instance, the message was previously different for an attempt to redefine a name whether this name was in the same section or not. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14528 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-07fsetdec : non-atomic elements are now transformed as variables first (fix #2464)letouzey
Btw, we also get rid of equalities on something else than elements or sets git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14525 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-07A new tactic is_var to check whether a term is a goal/section variableletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14524 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-07Fix bug #2557 and an issue with Propers for complementmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14523 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-07Remove 'status' of Program and explain the :> better, as well as referencing ↵msozeau
it properly in the syntax of terms git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14522 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-07Improved handling of element equalities in fsetdec (fix #2467)letouzey
- We now handle things like (H : E.eq x x -> ...) by rewriting E.eq x x into True. - There was also a confusion between E.t and its various equivalent (but syntactically different) forms. This should be solved by preventing inlining during an inner functor application. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14520 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-07ocamlbuild: remove -dllpath from coqrunbyteflagsglondu
See bug #2614. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14519 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-07ocamlbuild: Fix ocamlbuild compilation for changes to configure from r14500.glondu
The changes to myocamlbuild.ml didn't compile. See bug #2614. Signed-off-by: Tom Prince <tom.prince@ualberta.net> Signed-off-by: Stephane Glondu <steph@glondu.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14518 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-05Fixing Implicit Tactic mode damaged by commit r14496 (see also bug #2612).herbelin
There were some confusion on the role of clear_proofs which was applicable only to the global named_context. Hopefully made things clearer. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14517 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-05When a pattern match, don't use the first matching term but anherbelin
instance of the initial pattern (this fixes compilation of CoRN after r14499). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14516 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-05Removing vernacular code mistakenly committed.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14515 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-05Fixing critical inductive polymorphism bug found by Bruno.herbelin
If two distinct parameters of the inductive type contributes to polymorphism, they must have distinct names, othewise an aliasing problem of the form "fun x x => max(x,x)" happens. Also insisted that a parameter contributes to universe polymorphism only if the corresponding occurrence of Type is not hidden behind a definition. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14511 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-05Force dependency of Reference-Manual.pdf over Reference-Manual.dviherbelin
to ensure not only that several passes are done and the references are correct but also to avoid one of the targets Reference-Manual.dvi or Reference-Manual.pdf reading .aux files modified concurrently by the other target. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14510 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-05Use an ad-hoc monomorphic list in RelationClasses to avoid some universe ↵letouzey
constraints Patch by Robbert Krebbers (cf. #2611) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14509 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-05It happens that the type inference algorithm (pretyping) did not checkherbelin
that the return predicate of the match construction is at an allowed sort, resulting in tactics possibly manipulating ill-typed terms. This is now fixed, Incidentally removed in pretyping an ill-placed coercion. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14508 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-02Hash-consing of constr could share moreletouzey
- An inductive is hidden inside case_info. (btw, maybe we could get rid of this ci_ind altogether, since the information is already in the predicate of the match) - Typical situation where user kn and canonical kn are initially (==) was not preserved by hconsing of constant / mutual_inductive - inductive = (mutual_inductive * int) and constructor = inductive * int were not properly shared This should fix the strange situation of Udine/PiCalc taking *more* vo space after the last round of hcons tweaks. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14507 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-01Updating some links in the FAQherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14506 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-01Moving never-used comments from Zhints.v to dev/doc so as not toherbelin
obfuscate the standard library. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14505 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-01Fixing critical part of bug #2504. Not all inductive types in Type areherbelin
polymorphic and only for inductive polymorphic types is the conclusion of the arity irrelevant. Refreshing at discharge time (that indtypes.ml expects for retyping) should be done only for polymorphic types. For monomorphic inductive types in Type, the type level is possibly related to universe constraints stored in the section and it must not be changed. [Alternatively, discharge should not retype inductive types from scratch, but instead generalize them over the section variables, the same way it does for definitions/axioms. But that's another story.] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14501 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-27In Coq_config: get rid of coqsrc and make coqlib optionalglondu
I assume that once Coq is installed in non-local mode and run from its installed path, sources are no longer available. The coqsrc variable doesn't make any sense, then, and its intended value can always be inferred from Sys.executable_name. Moving it to Envars.coqroot. Make coqlib optional. Currently, it is set to None only in -local mode or with ocamlbuild. When set to None, -local layout is assumed (binaries in ./bin, library in .). The behaviour should not be changed when an explicit coqlib has been given to ./configure. This commit should make it possible to run a Coq compiled with -local from anywhere (no hard-coded absolute path embedded in the executables, intermediary step to bug #2565). It WILL BREAK settings re-using source trees after installation in non-local mode (are there actual use cases for that?). Hard-coded absolute paths still remain: - in the build system, so the need to re-run ./configure after moving the source tree is still expected for now; - in coqrunbyteflags, I think we are limited by ocaml itself; - docdir. All absolute paths should be removed, ultimately. As a side-effect, simplify computing of Envars.coqbin. I don't see any good reason to keep it as a function. Disclaimers: - initialization of Sys.executable_name is not consistent across all architectures; relying so much on it might trigger bugs. I'm pretty sure something will explode if one adds arbitrary symlinks on top of that; - ocamlbuild stuff not tested. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14500 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-26Added support for referring to subterms of the goal by pattern.herbelin
Tactics set/remember and destruct/induction take benefit of it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14499 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-26Generalizing subst_term_occ so that it supports an arbitrary matchingherbelin
function but also restricting it to closed matching and consequently renaming it to subst_closed_term_occ. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14498 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-26Adding subst_term up to convherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14497 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-26Moving implicit tactic support from Tacinterp to Pfedit and final evarherbelin
resolution from Tacinterp to Pretyping (close to resolve_evars) so that final evar resolution can eventually be called from Tactics. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14496 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-25Polishing commits r14492, r14448 and r14407 (tactics propagateherbelin
conversion hints to kernel). Whether REVERTcast must be known from coqchk is unclear. In the meantime, warn about the unstability of the situation (see also bug #2599). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14495 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-25Not hard-wiring camlp5 path in target source-doc!herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14494 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-24Applying Jean-Baptiste Rouquier's FAQ update proposed on coqdev aboutherbelin
using unicode in X11. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14493 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-24Completing r14448 and thus continuing r14407 (using Cast to propagateherbelin
information coming from tactics on how to solve cst/cst critical pairs in the kernel conversion machine). In r14448, extra Cast's were removed from kernel type-checker but (erroneously) not from the terms actually registered in the environment. The current commit completes the work by registering the term output by the type-checker and not the original term. Note that this needs to move hconsing from before to after typing. On the Coq library, propagating Cast (without keeping them on disk) induces a stable 1% speedup (Xeon w3540). Having hcons before or after type-checking makes no difference. It remains to test on user contribs whether the current commit compensates the slow down and vo size increasing coming with the improvement made to Qed in r14407. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14492 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-23Fix commit 14489: missing Coq. in dirpathletouzey
Kudos to Tom Prince for noticing this... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14491 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-23auto with nocore : disable the use of the core database (wish #2188)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14490 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-23Program: add some check_required_library (fix #2592) + some dead code removalletouzey
If these additional checks take too much time, maybe using true laziness instead of (fun () -> ...) could help. Btw, some other init_constant in Program would deserve preliminary check_required_library... I've also removed some unused delayed constr, at least one of them being erroneous git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14489 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-22Remove specific hash-consing of Term.types (was unused anyway)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14488 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-22Hash-consing: attempt to stop hash-consing separately constr in declare.mlletouzey
Now that Yann has provided a better hashing mechanism for constr, it might be interesting to (re-?)activate a global hash-consing of constr. Earlier, specific hash-cons tables were created at each call to hcons_constant_declaration. According to Hugo, this was meant to avoid blow-up in at least contrib Pocklington. This contrib seems to behave nicely now with global hashconsing (thanks Yann ;-). We'll see tomorrow what impact this has on other contribs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14487 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-22Remove duplicated version of check_required_library.letouzey
Signed-off-by: Tom Prince <tom.prince@ualberta.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14486 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-22test-suite : an additional message displayed by Notation2.vletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14485 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-22Fix test-suite for s/Defining '\1' as keyword/Identifier '\1' now a keyword/.letouzey
Signed-off-by: Tom Prince <tom.prince@ualberta.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14484 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-22Fixing bug #2606 (bad coqdoc processing of coq escaped in comments).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14482 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-19Makefile.doc: typo, index_url.txt should be index_urls.txtletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14481 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-19Fix test-suite/ide for repository compiled without -local (fix #2600)letouzey
- Add option -boot to the coqtop given to fake_ide - Be sure that a dying coqtop subprocess cannot go unnoticed. Before that, for repositories compiled without -local, coqtop -ideslave was dying immediately because it was missing its coqlib informations. Then the first command send via Marshal.to_channel was triggering a SIGPIPE and hence the death of fake_ide. Strangely, the return code was not necessarily understood as non-zero (?!). We now catch SIGPIPE and do an "exit 1". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14480 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-18avoid dependency nightmare by creating coqdep_{lexer,common}.mliletouzey
Sequel to commit 14476 : in fact, even with "tools" in .PHONY, we still may have coqdep stuff being recompiled in a "make" that follows a successful "make". This seems to related to the hacks I've introduced to prevent ocamlopt from erasing and recreating .cmi when there's no .mli around (cf. comment around line 823 in Makefile.build). Scenario: - First we build coqdep_boot directly out of coqdep_lexer.ml and co. When ocamlopt is around, this creates some .cmx and .cmi, but no .cmo. - Later we build coqdep, which need coqdep_lexer.cmx and co. Now "make" checks whether these .cmx are up-to-date. But our hacks made these .cmx depend on the corresponding .cmi. Then "make" checks whether these .cmi are up-to-date. But our hacks made these .cmi depend on the corresponding .cmo. These .cmo doesn't exist yet, we run ocamlc, which recreates the .cmi with same content but a different timestamp. For some strange reason, even with refreshed .cmi, the .cmx are not remade by this run, but will be on the next run. Conclusion: what a mess. Implicit rules about .cmx / .cmo / .cmi should be improved, but I see currently no simple solution. In the meantime, an simple ad-hoc fix is to create these two .mli ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14479 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-17doc/refman/Extraction.tex: no need to actually build euclid.mlletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14478 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-17Euclid: make the proof transparent (example of extraction in stdlib)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14477 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-17Various fixes in the Makefilesletouzey
After a successful build, re-doing make world should almost do nothing. For that: - Many targets added to .PHONY, especially "tools" since a "tools" directory exists. And anyway this is said to speed-up make a bit. - Concerning fake_ide, mentionning the .cm* instead of the .ml* avoid rebuilding these .cm*, and hence possibly many other things. - in Makefile.doc: fix the rule building index_url.txt - coqtop.* is now built by $(BESTCOQMKTOP) instead of $(COQMKTOP) (which is the symlink). This avoids a situation where a first "make" could redo just a few files while a second "make" will rebuild many more. Typical scenario : touch the Makefile, 1st make was re-doing tolink.ml and then coqmktop, but no more, a 2nd make was then detecting that coqtop and the stdlib was to be redone git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14476 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-16Omega: for non-arithmetical goals, try proving False from context (wish #2236)letouzey
This way, no more error messages like "Unrecognized predicate". Some code simplification and reorganization on the way, in particular a few tests like "is_Prop ..." or "closed0 ..." were actually useless. Also add support for the situation H:~Zne x y for uniformity. Beware: scripts relying negatively on the strength of omega may have to be adapted (e.g. "try omega. some_more_tactics_in_case_omega_fails."). For instance, one line deletion in PermutSetoid.v Probably more cumbersome : "auto with *" becomes stronger since it may call omega. Todo : check the impact on contribs tomorrow. Btw, this commit seems to solve a bug where omega was to be guided by some (set foo:= ...) before being able to succeed (cf PermutSetoid.v) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14474 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-15Omega aware of Z.pred (fix #1912)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14472 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-01 01:11:27 +0000