aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2011-05-05BinNat: N.binary_rect is now a definition instead of an opaque proofletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14111 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-05Peano recursion for positive: integration of Daniel Schepler's codeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14110 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-05Minimal lemmas about Z.gt, N.gt and coletouzey
The use of these predicate isn't recommended, but let's at least allow converting > >= and < <= git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14109 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-05Modularisation of Znat, a few name changed elsewhereletouzey
For instance inj_plus is now Nat2Z.inj_add git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14108 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-05BinInt: Z.add become the alternative Z.add'letouzey
It relies on Z.pos_sub instead of a Pos.compare followed by Pos.sub. Proofs seem to be quite easy to adapt, via some rewrite Z.pos_sub_spec. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14107 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-05Modularization of BinInt, related fixes in the stdlibletouzey
All the functions about Z is now in a separated file BinIntDef, which is Included in BinInt.Z. This BinInt.Z directly implements ZAxiomsSig, and instantiates derived properties ZProp. Note that we refer to Z instead of t inside BinInt.Z, otherwise ring breaks later on @eq Z.t git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14106 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-05Modularization of Nnatletouzey
For instance, nat_of_Nplus is now N2Nat.inj_add Note that we add an iter function in BinNat.N git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14105 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-05Setoid_ring: some cleanups related with BinPos and BinNatletouzey
In particular, positive_eq and N_eq and Neq_bool are now Pos.eqb and N.eqb git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14104 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-05Wf.iter_nat becomes Peano.nat_iter (with an implicit arg)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14103 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-05BinNatDef containing all functions of BinNat, misc adaptations in BinPosletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14102 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-05BinPosDef: a module with all code about positive, later Included in BinPosletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14101 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-05Modularization of BinNat + fixes of stdlibletouzey
A sub-module N in BinNat now contains functions add (ex-Nplus), mul (ex-Nmult), ... and properties. In particular, this sub-module N directly instantiates NAxiomsSig and includes all derived properties NProp. Files Ndiv_def and co are now obsolete and kept only for compat git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14100 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-05Modularization of Pnatletouzey
For instance, former Pplus_plus is now Pos2Nat.inj_add. As usual, compatibility notation are provided. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14099 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-05Modularization of BinPos + fixes in Stdlibletouzey
BinPos now contain a sub-module Pos, in which are placed functions like add (ex-Pplus), mul (ex-Pmult), ... and properties like add_comm, add_assoc, ... In addition to the name changes, the organisation is changed quite a lot, to try to take advantage more of the orders < and <= instead of speaking only of the comparison function. The main source of incompatibilities in scripts concerns this compare: Pos.compare is now a binary operation, expressed in terms of the ex-Pcompare which is ternary (expecting an initial comparision as 3rd arg), this ternary version being called now Pos.compare_cont. As for everything else, compatibility notations (only parsing) are provided. But notations "_ ?= _" on positive will have to be edited, since they now point to Pos.compare. We also make the sub-module Pos to be directly an OrderedType, and include results about min and max. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14098 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-05Definitions of positive, N, Z moved in Numbers/BinNums.vletouzey
In the coming reorganisation, the name Z in BinInt will be a module containing all code and properties about binary integers. The inductive type Z hence cannot be at the same location. Same for N and positive. Apart for this naming constraint, it also have advantages : presenting the three types at once is clearer, and we will be able to refer to N in BinPos (for instance for output type of a predecessor function on positive). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14097 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-05Zdiv: results about eqm (the equality modulo some N) under a sectionletouzey
These results are quite anecdotic, and may have bad interaction with the rest of the typeclass infrastructure. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14096 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-05Better comments and organisation in Datatypes.vletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14095 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-05Extraction: allow extraction foo when foo is an alias notationletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14094 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-05Fix merge, Cumul moved to CUMULmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14093 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-05Merge branch 'subclasses' into coq-trunkmsozeau
Stop using hnf_constr in unify_type, which might unfold constants that are marked opaque for unification. Conflicts: pretyping/unification.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14092 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-04First phase removing obsolete support for eta up to conversion inherbelin
"apply" unification. Assuming w_unify_0 is not eventually abandoned, it remains to merge unify_with_eta into unify_0 (what unify_with_eta does and that unify_0 does not do is to select of two instances of the same meta the one with less lambda's; it is unclear whether this is useful heuristic). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14091 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-03As many notation for for vectors as for List.pboutill
Tiny doc of mli-doc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14089 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-29when -camlbin is explicitly given in configure, $OCAML* are $CAMLBIN/exec.pboutill
Coq_makefile wrote $CAMLBIN twice... This should fix ssreflect in bench. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14088 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-29Fixed a bug causing inconsistent states during proof editting.aspiwack
Some toplevel commands (for instance the experimental bullets) are composed of several atomic commands, the failure of one must imply the failure of the whole toplevel command. This commit introduces a system of transaction to that effect. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14087 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-29Some comments.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14086 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-29Typo in test InitSyntax.outherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14085 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-29Choose relative directory over configured directory for coqlib.pboutill
This also fixes the bug where Util.error is always called, if coq searches for a relative directory. Signed-off-by: Tom Prince <tom.prince@ualberta.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14084 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-28Attempt to use more local doc in coqidepboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14083 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-28CHANGES updatepboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14082 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-28coq_makefile big cleanuppboutill
For everybody: variable customization should be easier. (Bug 2533 & more) For plugins: mli files are accepted, doc of them is done, ml4 files really work, ml files aren't camlp* preprocced, ready to build with camlp4 is your code is ready too, should work on any architecture nevermind the one on which you've done the coq_makefile. For others: html doc installation in $DOCDIR/users-contrib/"you"/ git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14081 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-28coqtop -config returns coq returns coq environments at exection timepboutill
It looks like a variables definition part of a Makefile. Names are from coq makefiles. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14080 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-28Revert r14078 "Partial backtrack on the support for open terms in ↵gmelquio
destruct/induction:" While this is needed for supporting destruct with typeclasses on 8.4, it was not my intent to commit it yet (as a better fix might be in the work), so reverting it for now. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14079 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-28Partial backtrack on the support for open terms in destruct/induction:gmelquio
use type classes to possibly solve evars before trying to unify the term (or the dependencies of its type) agains a subterm of the current goal. This solves compatibility bug #2222. Mixing unification and type classes is left for future work. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14078 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-28Coqide: try to properly send interrupts to coqtop on Win32letouzey
We use GenerateConsoleCtrlEvent(CTRL_C_EVENT,...) after having attached coqide to the console of the coqtop we want to interrupt. Two caveats: - This code isn't compatible with Windows < XP SP1. - It relies on the fact that coqide is now a true GUI app, without console by default. If for some reason the console of coqide is restored (for instance via mkwinapp -unset), strange behavior of the interrupt button is to be expected, at the very least all instances of coqtop will get Ctrl-C instead of a precise one. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14077 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-28Adding "Tactic Notation" in doc index.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14076 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-28Fixing an "apply -> ... in hyp" bug (the hyp was considered as a fixedherbelin
ident by Ltac). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14074 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-28Fixed notation printing bug when curly brackets are involved (requestsherbelin
for adding spaces were not taken into account in notations containing patterns of the form "{ ident symbol", paradoxically resulting in adding extra spaces, e.g. when printing the type "{ x | P x }" of "exist", due to interferences with the heuristic for adding breaking points in Metasyntax.make_hunk). Also adapted output of test InitSyntax.v after commit r14018 improved the printing of "ex P" and "sig P". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14073 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-27Updating CHANGESherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14072 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-27Fixing output of Notations2.v test messed up in r14060herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14071 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-26Pcoq.ml4: fix a typo in a comment to please ocamldocletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14070 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-26G_vernac can be parsed without grammar.cmaletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14069 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-26dev/base_include: no more mod_self_idletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14068 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-26Fixing commit r14061 (changes in file tactics.ml were mistakenly committed).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14067 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-26Coqide: fix remove_current_view_page (#2499)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14065 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-25Fix for handling of -R "" in coqdoc (bug #2423).herbelin
(submitted by Tom Prince <tom.prince@ualberta.net>) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14063 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-25Fixing and completing interpretation of let's in notations for iterated binders.herbelin
(backport from trunk) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14061 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-25Fixing and completing interpretation of let's in notations for iterated binders.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14060 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-24Yet another bug in printing fix with let-in bindersherbelin
(backport from branch v8.3) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14058 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-24Fixing bug in printing let-in binders in fix/cofixherbelin
(backport from branch v8.3) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14055 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-24Fixed a bug of destruct which was sometimes forgetting local definitions ↵herbelin
behind it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14053 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 08:14:05 +0000