aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2013-09-10Temporary fix of emacs mode for ProofGeneralletouzey
To the best of my knowledge, even with the latest cvs version of PG: - the goals must be finally displayed at each step - the <info>...</info> async feedback messages aren't handled yet. I'll check with Enrico what he intended with these two lines, but meanwhile let's comment them... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16767 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-07Change syntax of Hint Resolve to actually accept user-given priorities.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16766 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-06Moving Searchstack to CStack, and normalizing names a bit.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16765 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-05Optimizing some evar_maps manipulation. In particular, using a [map] insteadppedrot
of a [fold] in [nf_*] normalizing functions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16764 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-05Documentation of Evd.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16763 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-05Cleaning up of Evd. Extruding the tower of modules used to define evar_maps.ppedrot
They did not really enhance the safety of the code, as several outer parts acceeded directly to the internal representation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16762 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-04More robust argument setter in CoqIDE. It does not crash anymore on badppedrot
arguments. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16761 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-03Fixing some tests from the test-suite.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16760 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-03Partly replacing list-based access functions in Evd. This is stillppedrot
unsatisfactory as some functions implicitly require some ordering on the evars, but this is already better. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16759 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-03Some cleanup in Autoppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16758 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-02Removing more association lists in Constrintern.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16757 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-02* test-suite/success/Unicode_utf8:regisgia
Regression test for bug #3020. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16756 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-02* lib/Unicode:regisgia
Workaround. Some characters seems to be missing in Camomile's category tables. We add them manually. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16755 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-02* parsing/Lexer: Cosmetics.regisgia
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16754 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-02* configure: Remove trailing space.regisgia
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16753 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-30summary for ML modules made correctgareuselesinge
This summary entry is special because its unfreeze may load ML code that in turns adds summary entries. Hence it is the first summary piece to be unfreezed, otherwise some summaries may get lost. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16752 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-30add "Print Ring" and "Print Field" vernacular commandsgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16751 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-30Make the jopin-document button wait for slaves to terminategareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16750 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-30Fixing the code of field_simplify_eq.amahboub
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16749 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-30When PG is used as interface behave as before STMgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16748 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-30ind_tables: properly handling side effectsgareuselesinge
If a constant is defined as transparent, not only its side effects (opaque sub proofs as in abstract, and transparent ind schemes) are declared globally, but the ones that are schemes are also declared as such. The only sub optimal thing is that the code handling in a special way the side effects of transparent constants is in declare.ml that does not see ind_tables.ml, hence a forward ref to a function is used. IMO, ind_tables has no reason to stay in toplevel/. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16747 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-30recdef: restore old semantics (pre STM)gareuselesinge
The Stm commit switched from an home made handling of failures to a with_state_protection. This was wrong, since in case of success the global state has to be left altered. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16746 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-30Fix typo in error messagegareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16745 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-30safe Conv_oracle state for type checkinggareuselesinge
safe_typing is not purely functional, hence we cannot chain it as if it was a pure computation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16744 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-30Stm: if slave process dies badly go back to local lazy evaluationgareuselesinge
Processing the proof in a slave process may fail for an implementation error, e.g. the state could not be marshalled, or an anomaly is raised by the slave. In this case we fall back to local, lazy, evaluation in the master process. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16743 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-30-coq-slaves: close_on_exec + correct argument passinggareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16742 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-30Remove Obj.magic from safe typinggareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16741 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-30Trickyer test for Paral-ITPgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16740 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-28Fixing bug #3083.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16739 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-28Removing some lone List.assoc & List.mem in lib.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16738 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-25Removing association lists in Reductionops. Btw, defining the dual of theppedrot
domain operation on maps. The efficiency should just be improved. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16737 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-25Actually using the domain function for maps.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16736 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-25Added a more efficient way to recover the domain of a map.ppedrot
The extended signature is defined in CMap, and should be compatible with the old one, except that module arguments have to be explicitely named. The implementation itself is quite unsafe, as it relies on the current implementation of OCaml maps, even though that should not be a problem (it has not changed in ages). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16735 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-25Replacing lists by sets in clear tactic.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16734 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-23Adding dynamic value printing to votour through a registering mechanism.ppedrot
TODO: register the desired dynamic types. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16733 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-23Fix computation of discharged hyps for inductive types forgetting the ↵msozeau
conclusion of the arity. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16732 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-23Updating documentation of the ring/field tactics.amahboub
Removes the requirements that are obsolete after commit r16730. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16731 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-23Fixing an incompleteness of the ring/field tacticsamahboub
The problem occurs when a customized ring/field structure declared with a so-called "morphism" (see 24.5 in the manual) tactic allowing to reify (numerical) constants efficiently. When declaring a ring/field structure, the user can provide a cast function phi in order to express numerical constants in another type than the carrier of the ring. This is useful for instance when the ring is abstract (like the type R of reals) and one needs to express constants to large to be parsed in unary representation (for instance using a phi : Z -> R). Formerly, the completeness of the tactic required (phi 1) (resp. (phi 0)) to be convertible to 1 (resp. 0), which is not the case when phi is opaque. This was not documented untill recently but I moreover think this is also not desirable since the user can have good reasons to work with such an opaque case phi. Hence this commit: - adds two constructors to PExpr and FExpr for a correct reification - unplugs the optimizations in reification: optimizing reification is much less efficient than using a cast known to the tactic. TODO : It would probably be worth declaring IZR as a cast in the ring/field tactics provided for Reals in the std lib. The completeness of the tactic formerly relied on the fact that git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16730 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-22Correcting misplaced Proof command.amahboub
I did not even know it was possible to inline a 'Proof.' anywhere in a script. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16729 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-22Fixing a significant efficiency leak in the code of the field tactic.amahboub
The field tactic post-processes the data generated during normalization to ensure that vanished denominators do not cancel: essentially, this step removes duplicates from a list of polynomials and uses the clean list to generate the conjunction of associated non-zero conditions. This conjunction is the proof obligation the user has to prove by hand after a successful call to the field tactic. The computation of the proof obligation statement was performed using a fine-tuned reduction strategy, coded in the newring.ml4 file (see the fv-protect tactic). However, not only this strategy information was forgotten by the kernel, but the strategy used at Qed time caused a real explosion (examples normalized in 70s by the tactic have a one hour Qed). No idea why. The fix consists in opacifying the part of the goal irrelevant to computation and call the vm on the duplicate removal step. BTW this step is programmed in a naive way and can probably be made more efficient. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16728 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-22Nicer code concerning dirpaths and modpath around Libletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16727 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-22Misc changes around coqtop.ml :letouzey
- Revised Coqtop.parse_args in a cleaner and lighter style - Improved error message in case of argument parse failure: * tell which option is expecting a related argument * in case of unknown options, warn about them all at once * do not hide the previous error messages by filling the screen with usage(). Instead, suggest the use of --help. - Specialized boolean config field Coq_config.arch_is_win32 - Faster Envars.coqlib, which is back to (unit->string), and just access Flags.coqlib. Caveat: it must be initialized once via Envars.set_coqlib - Avoid keeping an opened channel to the "revision" file - Direct load of theories/init/prelude.vo, no detour via Loadpath Beware : ./configure must be runned after this commit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16726 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-22Less "Coq" strings everywhereletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16725 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-22micromega: remove empty file CheckerMakerletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16724 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-22More complete hashcons : lists (dirpath), arrays (constr)letouzey
Earlier, the elements of constr arrays were hash-consed, but not the array itself. This helps a bit when the same (f a1 ... an) is manipulated a lot : -20% in the size of opaque terms in Integral_domain.vo and Nsatz.vo Similarly it's interesting to hash-cons sub-lists for dirpaths, since in Coq.A.B and Coq.A.C we could share Coq.A. With this patch, the hash-consing of constr seems quasi-optimal: Pierre-Marie's marshal compactor is unable to shrink opaque tables by more than 2%, and this difference seems to be due to untyped compaction (for the compactor Rel 1 = Prop Pos). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16723 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-22Change in vo format : digest aren't Marshalled anymoreletouzey
Since digests are strings (of size 16), we just dump them now in vo files (cf. Digest.output) instead of using Marshal on them : this is cleaner and saves a few bytes. Increased VOMAGIC to clearly identify this change in the format. Please rerun ./configure after this commit. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16722 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-22Field_theory : faster and nicer proofs + nice notations.letouzey
This file should compile now twice as fast as earlier. A large part of this speedup comes from swithching to proofs without "auto" (and also improving them quite a lot). Nicer lemma statements thanks to notations and separate scopes (%ring, %coef, %poly). The Field_correct lemma lost some args (sign_theory ...) during the refactoring. After inspection, this looks legitimate, so I've hack the field tactic accordingly. The args were there probably due to some intuition or similar interfering with local vars. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16721 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-22Ring_polynom : shorter proof for Psub_okletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16720 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-20Partial revert of r16711letouzey
It seems that it's critical for the native compiler that a fresh (ref NotLinked) is created during substitution. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16719 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-20Fixing votourppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16718 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 20:12:11 +0000