aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Move stuff about positive into a distinct PArith subdirGravatar letouzey2010-11-02
| | | | | | | Beware! after this, a ./configure must be done. It might also be a good idea to chase any phantom .vo remaining after a make clean git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13601 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restored checking that _all_ arguments of the command line are meaningfulGravatar herbelin2010-11-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13600 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add tolerance for existential variables in Check.Gravatar herbelin2010-10-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13599 85f007b7-540e-0410-9357-904b9bb8a0f7
* An experimental support for open constrs in hints and in "using"Gravatar herbelin2010-10-31
| | | | | | | option of "auto". Works for not too complicated hints (e.g. "@pair _ _ 0"). Would be simpler if make_apply_entry supported lemmas containing evars. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13598 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleaning the use of parentheses around evd and evdref (cosmetic commit).Gravatar herbelin2010-10-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13597 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor code improvements around libobjectGravatar herbelin2010-10-31
| | | | | | | | - renamed load_object in mltop into load_ml_object to avoid confusion with load_object in library - flushed the liboject warning in real time git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13596 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor factorization of the part of the code used for Unnamed_thm saving.Gravatar herbelin2010-10-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13595 85f007b7-540e-0410-9357-904b9bb8a0f7
* Slight code cleaning in auto.ml (made code of make_exact_entry andGravatar herbelin2010-10-31
| | | | | | make_apply_entry more similar). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13594 85f007b7-540e-0410-9357-904b9bb8a0f7
* Slight cosmetic cleaning of tacred.ml.Gravatar herbelin2010-10-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13593 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add (quilt's) .pc to .gitignoreGravatar glondu2010-10-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13590 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove some unnecessary (?) "open Ideutils"Gravatar glondu2010-10-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13589 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove (unused) ide/highlight.mllGravatar glondu2010-10-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13588 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction of bug #2414 (report of r 13586)Gravatar jforest2010-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13587 85f007b7-540e-0410-9357-904b9bb8a0f7
* Compatibility camlp4/camlp5Gravatar herbelin2010-10-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13584 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fail, when successful, prints something only in verbose modeGravatar glondu2010-10-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13583 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix minor typo in error message (Closes: #2408)Gravatar glondu2010-10-25
| | | | | | Patch from Adam Megacz. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13577 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bug #2412, continued (preprocessing of Ltac Debug errorsGravatar herbelin2010-10-23
| | | | | | | forgotten in r13431). Sorry for having thought that the extra needed line could after all be not necessary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13576 85f007b7-540e-0410-9357-904b9bb8a0f7
* Used multiple lists of implicit arguments to transfer the choices ofGravatar herbelin2010-10-23
| | | | | | | | | | Program in terms of implicit arguments to the rest of the library. This commit only covers the case of list of implicit arguments that have a different length in Program (e.g. inl, Vcons) but not the case of implicit arguments which differs only in their maximality status (e.g. pair). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13575 85f007b7-540e-0410-9357-904b9bb8a0f7
* Automatically translate hints of the form "c _ ... _" into "c". BesidesGravatar herbelin2010-10-23
| | | | | | | being convenient, it improves compatibility when moving more implicit arguments to maximal status. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13574 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bug #2412 (preprocessing of Ltac Debug errors forgotten in r13431).Gravatar herbelin2010-10-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13573 85f007b7-540e-0410-9357-904b9bb8a0f7
* FMapFacts: typo noticed by AaronGravatar letouzey2010-10-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13572 85f007b7-540e-0410-9357-904b9bb8a0f7
* Still another Open Scope than should be LocalGravatar letouzey2010-10-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13571 85f007b7-540e-0410-9357-904b9bb8a0f7
* Solve name conflict about pow introduced by commit 13546.Gravatar letouzey2010-10-21
| | | | | | | - NPeano isn't Exported by default anymore (contains pow for nat). - in coq_micromega.ml, we specify more where to find the pow of R. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13569 85f007b7-540e-0410-9357-904b9bb8a0f7
* Still some more Cpow in Type rather than Set (cf. r13542)Gravatar letouzey2010-10-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13568 85f007b7-540e-0410-9357-904b9bb8a0f7
* Oups, new file Zsqrt_def was exporting Z_scopeGravatar letouzey2010-10-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13567 85f007b7-540e-0410-9357-904b9bb8a0f7
* Numbers: no need for advanced functions (e.g. sqrt) in NStrongRec, NDefOps, etcGravatar letouzey2010-10-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13565 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add sqrt in NumbersGravatar letouzey2010-10-19
| | | | | | | | | | | | | | | | | | | | | | As for power recently, we add a specification in NZ,N,Z, derived properties, implementations for nat, N, Z, BigN, BigZ. - For nat, this sqrt is brand new :-), cf NPeano.v - For Z, we rework what was in Zsqrt: same algorithm, no more refine but a pure function, based now on a sqrt for positive, from which we derive a Nsqrt and a Zsqrt. For the moment, the old Zsqrt.v file is kept as Zsqrt_compat.v. It is not loaded by default by Require ZArith. New definitions are now in Psqrt.v, Zsqrt_def.v and Nsqrt_def.v - For BigN, BigZ, we changed the specifications to refer to Zsqrt instead of using characteristic inequations. On the way, many extensions, in particular BinPos (lemmas about order), NZMulOrder (results about squares) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13564 85f007b7-540e-0410-9357-904b9bb8a0f7
* About "unsupported" unicode characters in notations.Gravatar herbelin2010-10-17
| | | | | | | | | - 8.2 (bug-fix): reverted check for unicode early at notation definition time (an unsupported "cadratin" space, 0x2003, was used in CoRN!) [by the way, what to do with unicode spacing characters in general?] - trunk: improved error message, removed redundant code git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13561 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix missing -coqlib argument to coqdep in test-suiteGravatar glondu2010-10-16
| | | | | | The test misc/deps-order was failing in non-local mode. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13560 85f007b7-540e-0410-9357-904b9bb8a0f7
* Support for GNU Make 3.82Gravatar glondu2010-10-16
| | | | | | Untested, see https://bugzilla.redhat.com/show_bug.cgi?id=631302 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13559 85f007b7-540e-0410-9357-904b9bb8a0f7
* Numbers : also axiomatize constants 1 and 2.Gravatar letouzey2010-10-14
| | | | | | | | | | | | | | | | | Initially, I was using notation 1 := (S 0) and so on. But then, when implementing by NArith or ZArith, some lemmas statements were filled with Nsucc's and Zsucc's instead of 1 and 2's. Concerning BigN, things are rather complicated: zero, one, two aren't inlined during the functor application creating BigN. This is deliberate, at least for the other operations like BigN.add. And anyway, since zero, one, two are defined too early in NMake, we don't have 0%bigN in the body of BigN.zero but something complex that reduce to 0%bigN, same for one and two. Fortunately, apply or rewrite of generic lemmas seem to work, even if there's BigZ.zero on one side and 0 on the other... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13555 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reparation du parseur/printer de nombres BigNGravatar letouzey2010-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13554 85f007b7-540e-0410-9357-904b9bb8a0f7
* Numbers: new functions pow, even, odd + many reorganisationsGravatar letouzey2010-10-14
| | | | | | | | | | | | | | | | | | | | | | | | - Simplification of functor names, e.g. ZFooProp instead of ZFooPropFunct - The axiomatisations of the different fonctions are now in {N,Z}Axioms.v apart for Z division (three separate flavours in there own files). Content of {N,Z}AxiomsSig is extended, old version is {N,Z}AxiomsMiniSig. - In NAxioms, the recursion field isn't that useful, since we axiomatize other functions and not define them (apart in the toy NDefOps.v). We leave recursion there, but in a separate NAxiomsFullSig. - On Z, the pow function is specified to behave as Zpower : a^(-1)=0 - In BigN/BigZ, (power:t->N->t) is now pow_N, while pow is t->t->t These pow could be more clever (we convert 2nd arg to N and use pow_N). Default "^" is now (pow:t->t->t). BigN/BigZ ring is adapted accordingly - In BigN, is_even is now even, its spec is changed to use Zeven_bool. We add an odd. In BigZ, we add even and odd. - In ZBinary (implem of ZAxioms by ZArith), we create an efficient Zpow to implement pow. This Zpow should replace the current linear Zpower someday. - In NPeano (implem of NAxioms by Arith), we create pow, even, odd functions, and we modify the div and mod functions for them to be linear, structural, tail-recursive. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13546 85f007b7-540e-0410-9357-904b9bb8a0f7
* Zeven: some complements, e.g. proofs that Zeven_bool and co are okGravatar letouzey2010-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13545 85f007b7-540e-0410-9357-904b9bb8a0f7
* NArith: add some functions Neven and NoddGravatar letouzey2010-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13544 85f007b7-540e-0410-9357-904b9bb8a0f7
* NArith: Definition of a Npow power functionGravatar letouzey2010-10-14
| | | | | | | | | | | | | By the way, adds an Piter_op iterator : Piter_op op p a is "a op a ... op a" with a occurring p times. It could be use to define Pmult_nat and hence nat_of_P (not fully done for maintaining compatibility). Unlike iter_pos, Piter_op is logarithmic in p, not linear. Note: We should adapt someday the brain-damaged Zpower to make it use Piter_op instead of iter_pos. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13543 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ring : Cpow in Type rather than Set (type of power coeffs in power_theory)Gravatar letouzey2010-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13542 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding test-case for bug #2362, which uses HO unification duringGravatar msozeau2010-10-12
| | | | | | | typeclass resolution. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13533 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #2393: allow let-ins inside telescopes (only fails when there'sGravatar msozeau2010-10-12
| | | | | | | no undefined variables in the context now). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13532 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backporting r13521 from branch 8.3 to trunk (fixing bug #2406, loopingGravatar herbelin2010-10-11
| | | | | | | on unsupported unicode character) + forbidding unsupported unicode in Notation declarations too. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13526 85f007b7-540e-0410-9357-904b9bb8a0f7
* More precise description of boolean ring in doc (see bug #2401)Gravatar glondu2010-10-11
| | | | | | | Also remove misleading example about classical propositional logic in "What does this tactic do?" section. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13523 85f007b7-540e-0410-9357-904b9bb8a0f7
* Export the "bullet" grammar entryGravatar glondu2010-10-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13519 85f007b7-540e-0410-9357-904b9bb8a0f7
* update CHANGES w.r.t. extractionGravatar letouzey2010-10-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13518 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug# 2392Gravatar msozeau2010-10-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13515 85f007b7-540e-0410-9357-904b9bb8a0f7
* TeX input method is now supported upstreamGravatar vgross2010-10-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13514 85f007b7-540e-0410-9357-904b9bb8a0f7
* test-suite: fix success/unification.vGravatar glondu2010-10-07
| | | | | | This test it not relevant anyway, thanks to eta... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13513 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing the Not_found error in bug #2404 + dead code removal in cases.mlGravatar herbelin2010-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13511 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove Explain* vernacsGravatar glondu2010-10-06
| | | | | | Basically untouched since 1999. Same fate as VernacGo (r13506). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13510 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: allow to use Extraction Inline / NoInline even from under a section.Gravatar letouzey2010-10-06
| | | | | | in addition, a makefile entry pluginsopt for compiling only the .cmxs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13509 85f007b7-540e-0410-9357-904b9bb8a0f7
* test-suite: fix output/Existentials.outGravatar glondu2010-10-06
| | | | | | | The new output makes sense with the new "1 subgoal = 1 evar" paradigm introduced with by the new proof engine. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13508 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 15:39:44 +0000