aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2013-09-20Update test for bug 2846 in order to use "Fail".xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16793 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-20Use "Fail" rather than rely on exit code.xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16792 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-19Uminus.v : prepare this test file for the use of Failletouzey
- Highlight the fact that the line defining "up" is the one which should fail. - Factor code with stdlib's Hurkens.v - This way, this test could become a "shouldnotfail" test by placing two final "Fail" (before the definitions of "up" and "paradox"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16791 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-19universes-buraliforti-redef.v : repair a match after Pierre B. syntax changesletouzey
This file, which is currently expected to fail at the last line (with Universe Inconsistency), was actually failing earlier after Pierre Boutillier changed the patterns (parameters are required now). A final "Fail" will soon arrives here to avoid such issue in the future... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16790 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-19Prettyp: avoid useless "let module"letouzey
As hinted by X. Clerc, a "let module" induces some runtime cost, so let's try to avoid them when possible. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16789 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-19Made the filename of compiled files explicit, i.e. add a ./ prefixppedrot
whenever the filename was given alone. This caused strange behaviour of coqtop that was compiling stuff we didn't want to just because it was somewhere in its loadpath. This is why FingerTree was not compiling, btw, as it had two files equally named in two different paths. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16788 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-19Get rid of the uses of deprecated OCaml elements (still remaining compatible ↵xclerc
with OCaml 3.12.1). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16787 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-18At least made the evar type opaque! There are still 5 remaining unsafeppedrot
casts of ints to evars. - 2 in Evarutil and Goal which are really needed, even though the Goal one could (and should) be removed; - 2 in G_xml and Detyping that are there for completeness sake, but that might be made anomalies altogether; - 1 in Newring which is quite dubious at best, and should be fixed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16786 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-18Removing the last global evar generation in Term_dnet. The veryppedrot
fact that the previous implementation was working is still black magic to me, as evars may have collided in intriguing ways... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16785 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-18Removing unused code from Term_dnet.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16784 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-18Removing almost all new_untyped_evar, and a bunch of Evd.add.ppedrot
Ultimately all evars should be created with respect to a given evar map, instead of using a global counter. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16783 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-18Taming the simpl evar hack that used to use negative evars.ppedrot
Now we just generate evars in the given evar map. At least, the test-suite isn't broken... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16782 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-14Slightly more compact representation of 'a substituted type,ppedrot
removing an unneeded indirection. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16781 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-13When Coq is reset-initialed by CoqIDE, do reset jobs countersgareuselesinge
Coq is not going to send any feedback message for the brute-force canceled jobs, given that the process was killed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16780 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-13fix error reporting window size calculationgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16779 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-13CoqIDE: new async error reporting window and slaves statusgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16778 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-13STM pretty printer should never failgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16777 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-13fix STM feeback on running jobsgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16776 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-13Do no compage wg_Notebook terms with (=)gareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16775 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-12Unplugging Autoinstance. The code is still here if someone wishesppedrot
to fix it, but it should be eventually erased. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16774 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-12CoqIDE: show number of proofs being checked in backgroundgareuselesinge
good test: Nijmegen/QArithSternBrocot/Zaux.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16773 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-12Minimal implementation of `Shallow marshalling of Libgareuselesinge
Just sufficient to make abstract work in such an (empty) lib. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16772 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-12Unknown commands starting a proof were not setting the proof mode.gareuselesinge
Fixes Orsay/Containers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16771 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-12Remove outdated commentgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16770 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-12VernacList handling was lost in STM mergegareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16769 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-12Fix bug in CStack introduced by refactoringgareuselesinge
Refactorings should be tested, right? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16768 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 18:25:02 +0000