aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2010-01-28Correction du bug #2219: application du patch envoyé par F. Garillotnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12695 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-28Backport fixes in Instance declarations to Program Instance.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12694 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-26Support for generalized rewriting under dependent binders, using themsozeau
[forall_relation] combinator. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12693 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-26Quick fix for references to section variables unbound in the currentmsozeau
environment during unification. Should be checked earlier. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12692 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-26Add [Next Obligation with tactic] support (wish #1953).msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12691 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-26make init + NMake.v/NMake_gen.vnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12690 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-26Add -makecmd configure optionglondu
This allows choosing gmake on *BSD (patch from Nima Hoda). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12689 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-25NMake (and hence BigN): shiftr, shiftl now in the signature NSigletouzey
we export the "safe" version of these functions, working for all input and not only reasonably small shifting arg. The former "unsafe" shiftr and shiftl are now unsafe_shiftr and unsafe_shiftl. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12688 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-25NMake: several things need not be macro-generatedletouzey
The macro-generated .v file is now NMake_gen.v, while NMake.v now contain the static things (i.e. definition of gcd via mod). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12687 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-19Ring31 : a ring structure and tactic for int31letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12685 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-19NMake_gen: fix previous commit (some spaces were critical), remove some more ↵letouzey
spaces git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12684 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-19NMake_gen: no more spaces at end of linesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12683 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-19Various bug fix on recent features of the module system:soubiran
- Include Self and equivalence of names - Include type in modules and nametab - Bang operator and composition of substitution git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12682 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-18More improvements of BigN, BigZ, BigQ:letouzey
- ring/field: detection of constants for ring/field, detection of power, potential use of euclidean division. - for BigN and BigZ, x^n now takes a N as 2nd arg instead of a positive - mention that we can use (r)omega thanks to (ugly) BigN.zify, BigZ.zify. By the way, BigN.zify could still be improved (no insertion of positivity hyps yet, unlike the original zify). - debug of BigQ.qify (autorewrite was looping on spec_0). - for BigQ, start of a generic functor of properties QProperties. - BigQ now implements OrderedType, TotalOrder, and contains facts about min and max. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12681 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-17BigN, BigZ, BigQ: presentation via unique module with both ops and propsletouzey
We use the <+ operation to regroup all known facts about BigN (resp BigZ, ...) in a unique module. This uses also the new ! feature for controling inlining. By the way, we also make sure that these new BigN and BigZ modules implements OrderedTypeFull and TotalOrder, and also contains facts about min and max (cf. GenericMinMax). Side effects: - In NSig and ZSig, specification of compare and eq_bool is now done with respect to Zcompare and Zeq_bool, as for other ops. The order <= and < are also defined via Zle and Zlt, instead of using compare. Min and max are axiomatized instead of being macros. - Some proofs rework in QMake - QOrderedType and Qminmax were in fact not compiled by make world Still todo: OrderedType + MinMax for BigQ, etc etc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12680 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-17Simplification of OrdersTac thanks to the functor application ! with no inlineletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12679 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-17Variant !F M for functor application that does not honor the Inline declarationsletouzey
For F(X:T), the application !F M works as F M, except that if module type T contains some "Inline" annotations, they are not taken in account when substituting X with M in F. See forthcoming commits for examples of use for this feature. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12678 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-15Report de la révision #12676notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12677 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-14Fix uncaught exceptionvgross
On windows platform, exceptions are not always encoded in utf-8, thus failing the assert. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12675 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-14Document Local Declare ML Moduleglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12674 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-14Avoid some more re-declarations of Equivalence instancesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12671 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-14Rename Zbinary into Zdigit in order to avoid confusion with ↵letouzey
Numbers/.../ZBinary.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12670 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-14Fix bug #2086, error message when we match on an non-inductive type.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12669 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-14- Show Obligation Tacticmsozeau
- fix bug #1952. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12668 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-14Add *.annot to .gitignoreglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12667 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-14Disable validateglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12666 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-13Try to avoid re-declaring Equivalence, especially for Logic.eqletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12662 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-12GenericMinMax: still a min_case_strong with hypothesis in the wrong orderletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12661 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-12g_decl_mode: 'by' is now a keywordletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12660 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-12Removing some betaiota-redexes in error messages (an experiment)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12659 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-12New version of 12650 that was broken (supporting again records whenherbelin
descending dependent conjunctions). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12658 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-12Typo in error messageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12657 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-12MSets: Class Ok becomes a definition instead of an inductive (thanks Matthieu)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12656 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-12Added module sharing support for typeclasses and hints (pri_auto_tactic).soubiran
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12655 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-12Numbers/.../NDefOps: one more property about ltbletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12654 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-12Numbers: some more proofs about sub,add,le,lt for natural numbersletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12653 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-12Numbers: two more Local Obligation Tacticletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12652 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-12revert commit 12650 for the moment, since it breaks MSetAVLletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12651 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-12Temporary fix to compensate the loss of descent on dependentherbelin
conjunctions (defined records now supported again but not unregistered ones). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12650 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-11Revert "Isolation of proof-displaying code"vgross
This reverts commit 8162ee31152eb2f99af724e88a7e15a899c17811. Not the smartest thing to do on the verge of tagging. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12649 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-11Isolation of proof-displaying codevgross
The formatting logic is now isolated in ide/proofBrowser.ml, and the goal printing logic is deported inside ide/coq.ml. Also, the proof mode special printing has been cut out. Finally, turn every call to show_goals_full into show_goals, and use show_goals_full as the body of show_goals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12648 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-11Support "Local Obligation Tactic" (now the default in sections).msozeau
Update Numbers that was implicitely using [simpl_relation] instead of the default tactic [program_simpl]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12647 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-08Numbers: BigN and BigZ get instantiations of all properties about div and modletouzey
NB: for declaring div and mod as a morphism, even when divisor is zero, I've slightly changed the definition of div_eucl: it now starts by a check of whether the divisor is zero. Not very nice, but this way we can say that BigN.div and BigZ.div _always_ answer like Zdiv.Zdiv. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12646 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-08* Segmenttree: New. A very simple implementation of segment trees.regisgia
* Unicodetable: Update with the standard table for lower case conversion. * Util: Rewrite "lowercase_unicode" to take the entire unicode character set into account. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12645 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-08Numbers: axiomatization + generic properties of abs and sgn.letouzey
This allow to really finish files about division. An abs and sgn is added to BigZ. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12644 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-08Init/Logic: commutativity and associativity of /\ and \/letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12643 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-08NZAxioms plus a compare allows to build an OrderedTypeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12642 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-07Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders*letouzey
Old stuff DecidableType.v and OrderedType.v stay there and keep their names for the moment, for compatibility. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12641 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-07Include can accept both Module and Module Typeletouzey
Syntax Include Type is still active, but deprecated, and triggers a warning. The syntax M <+ M' <+ M'', which performs internally an Include, also benefits from this: M, M', M'' can be independantly modules or module type. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12640 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-07Numbers: separation of funs, notations, axioms. Notations via module, ↵letouzey
without scope. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12639 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-24 19:16:05 +0000