aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* ocamlbuild: remove -dllpath from coqrunbyteflagsGravatar glondu2011-10-07
| | | | | | See bug #2614. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14519 85f007b7-540e-0410-9357-904b9bb8a0f7
* ocamlbuild: Fix ocamlbuild compilation for changes to configure from r14500.Gravatar glondu2011-10-07
| | | | | | | | | | | 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
* Fixing Implicit Tactic mode damaged by commit r14496 (see also bug #2612).Gravatar herbelin2011-10-05
| | | | | | | | 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
* When a pattern match, don't use the first matching term but anGravatar herbelin2011-10-05
| | | | | | | 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
* Removing vernacular code mistakenly committed.Gravatar herbelin2011-10-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14515 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing critical inductive polymorphism bug found by Bruno.Gravatar herbelin2011-10-05
| | | | | | | | | | | | 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
* Force dependency of Reference-Manual.pdf over Reference-Manual.dviGravatar herbelin2011-10-05
| | | | | | | | | 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
* Use an ad-hoc monomorphic list in RelationClasses to avoid some universe ↵Gravatar letouzey2011-10-05
| | | | | | | | 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
* It happens that the type inference algorithm (pretyping) did not checkGravatar herbelin2011-10-05
| | | | | | | | | | 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
* Hash-consing of constr could share moreGravatar letouzey2011-10-02
| | | | | | | | | | | | | | | | | - 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
* Updating some links in the FAQGravatar herbelin2011-10-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14506 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moving never-used comments from Zhints.v to dev/doc so as not toGravatar herbelin2011-10-01
| | | | | | obfuscate the standard library. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14505 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing critical part of bug #2504. Not all inductive types in Type areGravatar herbelin2011-10-01
| | | | | | | | | | | | | | 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
* In Coq_config: get rid of coqsrc and make coqlib optionalGravatar glondu2011-09-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* Added support for referring to subterms of the goal by pattern.Gravatar herbelin2011-09-26
| | | | | | 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
* Generalizing subst_term_occ so that it supports an arbitrary matchingGravatar herbelin2011-09-26
| | | | | | | 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
* Adding subst_term up to convGravatar herbelin2011-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14497 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moving implicit tactic support from Tacinterp to Pfedit and final evarGravatar herbelin2011-09-26
| | | | | | | 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
* Polishing commits r14492, r14448 and r14407 (tactics propagateGravatar herbelin2011-09-25
| | | | | | | | 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
* Not hard-wiring camlp5 path in target source-doc!Gravatar herbelin2011-09-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14494 85f007b7-540e-0410-9357-904b9bb8a0f7
* Applying Jean-Baptiste Rouquier's FAQ update proposed on coqdev aboutGravatar herbelin2011-09-24
| | | | | | using unicode in X11. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14493 85f007b7-540e-0410-9357-904b9bb8a0f7
* Completing r14448 and thus continuing r14407 (using Cast to propagateGravatar herbelin2011-09-24
| | | | | | | | | | | | | | | | | | | | | 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
* Fix commit 14489: missing Coq. in dirpathGravatar letouzey2011-09-23
| | | | | | 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
* auto with nocore : disable the use of the core database (wish #2188)Gravatar letouzey2011-09-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14490 85f007b7-540e-0410-9357-904b9bb8a0f7
* Program: add some check_required_library (fix #2592) + some dead code removalGravatar letouzey2011-09-23
| | | | | | | | | | | | | 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
* Remove specific hash-consing of Term.types (was unused anyway)Gravatar letouzey2011-09-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14488 85f007b7-540e-0410-9357-904b9bb8a0f7
* Hash-consing: attempt to stop hash-consing separately constr in declare.mlGravatar letouzey2011-09-22
| | | | | | | | | | | | 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
* Remove duplicated version of check_required_library.Gravatar letouzey2011-09-22
| | | | | | 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
* test-suite : an additional message displayed by Notation2.vGravatar letouzey2011-09-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14485 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix test-suite for s/Defining '\1' as keyword/Identifier '\1' now a keyword/.Gravatar letouzey2011-09-22
| | | | | | 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
* Fixing bug #2606 (bad coqdoc processing of coq escaped in comments).Gravatar herbelin2011-09-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14482 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile.doc: typo, index_url.txt should be index_urls.txtGravatar letouzey2011-09-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14481 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix test-suite/ide for repository compiled without -local (fix #2600)Gravatar letouzey2011-09-19
| | | | | | | | | | | | | | - 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
* avoid dependency nightmare by creating coqdep_{lexer,common}.mliGravatar letouzey2011-09-18
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* doc/refman/Extraction.tex: no need to actually build euclid.mlGravatar letouzey2011-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14478 85f007b7-540e-0410-9357-904b9bb8a0f7
* Euclid: make the proof transparent (example of extraction in stdlib)Gravatar letouzey2011-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14477 85f007b7-540e-0410-9357-904b9bb8a0f7
* Various fixes in the MakefilesGravatar letouzey2011-09-17
| | | | | | | | | | | | | | | | | | | 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
* Omega: for non-arithmetical goals, try proving False from context (wish #2236)Gravatar letouzey2011-09-16
| | | | | | | | | | | | | | | | | | 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
* Omega aware of Z.pred (fix #1912)Gravatar letouzey2011-09-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14472 85f007b7-540e-0410-9357-904b9bb8a0f7
* Re-allowing assumptions during proofs seems safe now (fix #2411)Gravatar letouzey2011-09-15
| | | | | | | | | | | | | This restriction was introduce to solve #808, whose underlying issue (causing a anomaly) doesn't seem active anymore. Semantic: - Axiom in the middle of a proof : immediatly usable (just as a Definition) - Hypothesis or Variable : not visible in current proof, only usable in the next ones. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14470 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqc: Recognize option -force-load-proofs.Gravatar letouzey2011-09-15
| | | | | | Signed-off-by: Tom Prince <tom.prince@ualberta.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14469 85f007b7-540e-0410-9357-904b9bb8a0f7
* Names.make_mbid and co : convert from/to identifier (avoid some String.copy)Gravatar letouzey2011-09-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14468 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using ↵Gravatar aspiwack2011-09-12
| | | | | | the uid returned by Goal.uid. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14467 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction du bug 2047Gravatar jforest2011-09-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14465 85f007b7-540e-0410-9357-904b9bb8a0f7
* More twicks on hash-consingGravatar letouzey2011-09-08
| | | | | | | | | | | | | | | | | | | | | | - When hash-consing, seeing ident as having string as sub-structure induces a penalty: two searchs are done in two tables (one for string, one for id). We simply say now that the hcons function for ident is the one for string - use more == during hash-consing of Names.uniq_ident and Names.module_path - clarification concerning hash-cons of Names.constant and Names.mutual_inductive: we only hash-cons the canonical part, but == could be used nonetheless on the obtained pair. Simply note that canonical_con of hash-consed constants will produce kernel_names that may be (=) but not (==). - Code cleanup : no direct use of string hash-consing apart in Names, we hence simplify hcons_names git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14464 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix the hconsing of universesGravatar letouzey2011-09-07
| | | | | | | | | | | | | | | | | Two issues were preventing the hcons1_univ function to properly work - a launch of Names.hcons_names () at each hconsing of universe, hence one separated hash-table for dir-path created at each time, oups... - Bad handling of the universe sub-structure universe_level To check : is there an interest in making separate calls to Names.hcons_names () in separate places (Univ, Term, Declare) ? I think not. Btw the hconsing of Declare.hcons_constant_declaration is also probably wrong. To be fixed in a forthcoming patch. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14463 85f007b7-540e-0410-9357-904b9bb8a0f7
* make world now builds fake_ide (to please coq-bench)Gravatar letouzey2011-09-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14462 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improved ltac code for zify (fix #2575).Gravatar letouzey2011-09-06
| | | | | | | | Note nonetheless that the underlying bug is still active (cf. #2602), I've just written the ltac stuff in a nicer way (no nested match goal), and things happen to work now :-) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14461 85f007b7-540e-0410-9357-904b9bb8a0f7
* test-suite/ide: misc improvementGravatar letouzey2011-09-06
| | | | | | | - make clean really erases *.log - some missing \n at end of files git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14460 85f007b7-540e-0410-9357-904b9bb8a0f7
* Avoid registering λ and Π as keywords just for some private Local NotationGravatar letouzey2011-09-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14459 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 17:35:41 +0000