aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* 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
* Remove ide/coq_tactics.ml*Gravatar glondu2010-10-06
| | | | | | | Unused and refers to pre-v8 tactics. Basically untouched since 2003. Most likely obsolete. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13507 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove VernacGoGravatar glondu2010-10-06
| | | | | | | | | | | | | | | | I agree with Arnaud on this one... Archeology: I could trace it back to r133 (in 1999!), and it was adapted to many big changes, including change of parsing (r2722, in 2002). Maybe it was used by Centaur or something similar once... The only relevant occurrences of "Go" in SVN history (since initial commit in 1999) is that it "semble peu robuste aux erreurs", without a clear specification of what it is supposed to do... Looks like an interesting feature, though, but needs complete rethinking (and documentation) with the new engine. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13506 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove unused unshare_proof_tree from xml pluginGravatar glondu2010-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13505 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove open_subgoals field of proof_treeGravatar glondu2010-10-06
| | | | | | It looks obsolete, probably as a consequence of the new proof engine. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13504 85f007b7-540e-0410-9357-904b9bb8a0f7
* (Hopefully) clearer explanation of Ltac's context patternsGravatar glondu2010-10-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13503 85f007b7-540e-0410-9357-904b9bb8a0f7
* test-suite: fix success/Typeclasses.vGravatar glondu2010-10-05
| | | | | | Obviously broken since r13359 (remove native Π)... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13502 85f007b7-540e-0410-9357-904b9bb8a0f7
* test-suite: fix success/AdvancedCanonicalStructure.vGravatar glondu2010-10-05
| | | | | | | I have no idea how this test could have ever worked... (ssreflect? declarative mode?) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13501 85f007b7-540e-0410-9357-904b9bb8a0f7
* Export definition of type implicits_list for contribs + fixed aGravatar herbelin2010-10-05
| | | | | | | discharge bug of implicit arguments related to commit 13484 (multiple implicit arguments sequences patch). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13500 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reintroduce kind_of_type (used by Presburger contrib)Gravatar glondu2010-10-05
| | | | | | This partially reverts commit r13467. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13497 85f007b7-540e-0410-9357-904b9bb8a0f7
* Auto-inlining of f_terminate in FunctionGravatar jforest2010-10-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13496 85f007b7-540e-0410-9357-904b9bb8a0f7
* test-suite: use unified diff output and use expected output as referenceGravatar glondu2010-10-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13495 85f007b7-540e-0410-9357-904b9bb8a0f7
* Forgotten lifts in eta-expansionGravatar glondu2010-10-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13494 85f007b7-540e-0410-9357-904b9bb8a0f7
* Install a printer for fconstr (ppconstr was installed twice)Gravatar glondu2010-10-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13493 85f007b7-540e-0410-9357-904b9bb8a0f7
* Two [Evd.fold] turned into [Evd.fold_undefined].Gravatar aspiwack2010-10-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13491 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bugs in previous commits about implicit arguments:Gravatar herbelin2010-10-04
| | | | | | | | | - fixing r13483 (supposed dead code in impargs was actually half-living: implicit arguments mode should merge with the {...} manually given implicit arguments but not with the "Implicit Arguments [...]" arguments), - fixing code of drop_first_implicits in r13484. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13490 85f007b7-540e-0410-9357-904b9bb8a0f7
* Avoid raising an anomaly when an error encapsulated with a dummyGravatar herbelin2010-10-03
| | | | | | location is raised from a loaded/compiled file! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13488 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test for non-regression of the display bug fixed in r13486.Gravatar herbelin2010-10-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13487 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing printing of module_path names (was using a debuggingGravatar herbelin2010-10-03
| | | | | | message since r11177). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13486 85f007b7-540e-0410-9357-904b9bb8a0f7
* Using multiple lists of implicit arguments in Program for preservingGravatar herbelin2010-10-03
| | | | | | | | | | | | | | the compatibility with the rest of the theories. Used multiple lists of implicit arguments in Init only when the maximality status is not modified in Program (and thus the compatibility is strictly preserved). This improves the compatibility for the implicit arguments of eq_refl and JMeq_refl between 8.2 and 8.3 when using Program (up to the residual differences in the maximality status). For the constants Acc_inv, inl, inr, left, right, Vnil, Vcons, the compatibility with 8.2 is not improved but the consistency between Program and the rest of the library is. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13485 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added multiple implicit arguments rules per name.Gravatar herbelin2010-10-03
| | | | | | | | | Example: "Implicit Arguments eq_refl [[A] [x]] [[A]]". This should a priori be used with care (it might be a bit disturbing seeing the same constant used with apparently incompatible signatures). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13484 85f007b7-540e-0410-9357-904b9bb8a0f7
* Dead code in impargs (afaics, no more need, since r11242, to mergeGravatar herbelin2010-10-03
| | | | | | automatic and manual implicit arguments twice). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13483 85f007b7-540e-0410-9357-904b9bb8a0f7
* Making display of various informations about constants more modular:Gravatar herbelin2010-10-03
| | | | | | | | | | | | | | - use list of non-newline-ended phrases instead of newline-separated texts because newline-separated texts does not support well being put in boxes (e.g. ''v 2 (str"a" ++ fnl()) ++ str"b" ++ fnl()'' prints "b" at indentation 2 while to get the expected output, one would have needed to have the fnl outside the box as in ''v 2 (str"a") ++ fnl() ++ str"b" ++ fnl()'' - also reason over lists of explicitly non-empty lines instead of checking for "mt" lines to skip The reason of this is to permit nesting of printing infos. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13482 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed a little printing bug with "About" on an undefined constant.Gravatar herbelin2010-10-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13481 85f007b7-540e-0410-9357-904b9bb8a0f7
* Simplify tactic(_)-bound arguments in TACTIC EXTEND rulesGravatar glondu2010-09-30
| | | | | | | | | | | | | | Arguments bound with tactic(_) in TACTIC EXTEND rules are now of type glob_tactic_expr, instead of glob_tactic_expr * tactic. Only the first component is kept, the second one can be obtained with Tacinterp.eval_tactic. Rationale: these declare parsing rules, and eval_tactic is a semantic action, and therefore should be done in the rule body instead. Moreover, having the glob_tactic_expr and its evaluation captured by these rules was quite confusing IMHO. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13480 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improve handling of metas as evars in unification (patch by Hugo)Gravatar letouzey2010-09-30
| | | | | | | Pratical situation: simple eapply foo on a goal ?123, while foo is a (forall f, exists ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13479 85f007b7-540e-0410-9357-904b9bb8a0f7
* Speed-up refine by avoiding some calls to Evd.foldGravatar letouzey2010-09-30
| | | | | | | | | | | Instead of the full Evd.fold, Evd.fold_undefined seems enough in - Evarutil.push_dependent_evars - the nf_evars call in Evarutil.evars_to_metas (we hence create a function nf_evars_undefined and use it there) This should bring back Compcert into reasonable compilation time git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13478 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #2321, allowing "_" named projections in classes. Not realizingGravatar msozeau2010-09-28
| | | | | | | | the wish to allow named projections to not be put in the canonical structures databases for Structures. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13474 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 01:13:36 +0000