aboutsummaryrefslogtreecommitdiff
path: root/plugins/setoid_ring
AgeCommit message (Collapse)Author
2013-02-19Dir_path --> DirPathletouzey
Ok, this is merely a matter of taste, but up to now the usage in Coq is rather to use capital letters instead of _ in the names of inner modules. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16221 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-18Minor code cleanups, especially take advantage of Dir_path.is_emptyletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16210 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
native OCaml code. Warning: the "retroknowledge" mechanism has not been ported to the native compiler, because integers and persistent arrays will ultimately be defined as primitive constructions. Until then, computation on numbers may be faster using the VM, since it takes advantage of machine integers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16136 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-18Unset Asymmetric Patternspboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16129 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-18Modulification of Labelppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16097 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-14Modulification of dir_pathppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16072 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-14Modulification of identifierppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-14Moved Stringset and Stringmap to String namespace.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16068 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-26Change Hint Resolve, Immediate to take a global reference as argumentmsozeau
instead of a general constr: this is the most common case and does not loose generality (one can simply define constrs before Hint Resolving them). Benefits: - Natural semantics for typeclasses, not class resolution needed at Hint Resolve time, meaning less trouble for users as well. - Ability to [Hint Remove] any hint so declared. - Simplifies the implementation as well. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15930 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-16Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterpletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15896 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15844 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-14As r15801: putting everything from Util.array_* to CArray.*.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15804 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
List module. That way, an "open Util" in the header permits using any function of CList in the List namespace (and in particular, this permits optimized reimplementations of the List functions, as, for example, tail-rec implementations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15801 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-08Updating headers.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-19Getting rid of the undocumented [complete] tactic, which wasppedrot
redundant with [solve]. The AST node still exists in Ltac, because this is used by the [assert ... by ...] tactical. Fixes #2847. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15625 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-07Ring_polynom : a restricted simpl instead of a unfold;foldletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15545 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-05Legacy Ring and Legacy Field migrated to contribsletouzey
One slight point to check someday : fourier used to launch a tactic called Ring.polynom in some cases. It it crucial ? If so, how to replace with the setoid_ring equivalent ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15524 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-05rewrite_db : a first attempt at using rewrite_strat for a quicker autorewriteletouzey
rewrite_db fails if nothing has been rewritten, and it only performs *one* top-down pass. For the moment, use (repeat rewrite_db) for emulating more closely autorewrite. Btw, let's make Himsg.explain_ltac_call_trace robust wrt TacExtend with fun(ny) parts git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15522 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-05More cleanup in Ring_polynom and EnvRingletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15521 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-05Kills the useless tactic annotations "in |- *"letouzey
Most of these heavyweight annotations were introduced a long time ago by the automatic 7.x -> 8.0 translator git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15518 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-05Open Local Scope ---> Local Open Scope, same with Notation and aliiletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15517 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
- For instance, refl_equal --> eq_refl - Npos, Zpos, Zneg now admit more uniform qualified aliases N.pos, Z.pos, Z.neg. - A new module BinInt.Pos2Z with results about injections from positive to Z - A result about Z.pow pushed in the generic layer - Zmult_le_compat_{r,l} --> Z.mul_le_mono_nonneg_{r,l} - Using tactic Z.le_elim instead of Zle_lt_or_eq - Some cleanup in ring, field, micromega (use of "Equivalence", "Proper" ...) - Some adaptions in QArith (for instance changed Qpower.Qpower_decomp) - In ZMake and ZMake, functor parameters are now named NN and ZZ instead of N and Z for avoiding confusions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15515 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
were closed (i.e. the only remaining ones are those of printing/parsing). Meanwhile, a simplified interface is provided in loc.mli. This also permits to put Pp in Clib, because it does not depend on CAMLP4/5 anymore. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15475 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-12Changed encoding from ISO-8859-1 to UTF-8 for some remaining gallina files.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15431 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-01Getting rid of Pp.msgnl and Pp.message.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15412 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-30Getting rid of Pp.msgppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15400 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29place all files specific to camlp4 syntax extensions in grammar/letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15387 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in ↵letouzey
grammar.cma git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15384 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstrletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15375 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
Corresponding operations in locusops.ml and miscops.ml The type of occurrences is now a clear algebraic one instead of a bool*list hard to understand. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15372 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-14Everything compiles again.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15034 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-02Noise for nothingpboutill
Util only depends on Ocaml stdlib and Utf8 tables. Generic pretty printing and loc functions are in Pp. Generic errors are in Errors. + Training white-spaces, useless open, prlist copies random erasure. Too many "open Errors" on the contrary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-12Proof using ...gareuselesinge
New vernacular "Proof using idlist" to declare the variables to be discharged at the end of the current proof. The system checks that the set of declared variables is a superset of the set of actually used variables. It can be combined in a single line with "Proof with": Proof with .. using .. Proof using .. with .. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14789 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-17Fixing bug #2640 and variants of it (inconsistency between when andherbelin
how the names of an ltac expression are globalized - allowing the expression to be a constr and in some initial context - and when and how this ltac expression is interpreted - now expecting a pure tactic in a different context). This incidentally found a Ltac bug in Ncring_polynom! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14676 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-02Add type annotations around all calls to Libobject.declare_objectletouzey
These annotations are purely optional, but could be quite helpful when trying to understand the code, and in particular trying to trace which which data-structure may end in the libobject part of a vo. By the way, we performed some code simplifications : - in Library, a part of the REQUIRE objects was unused. - in Declaremods, we removed some checks that were marked as useless, this allows to slightly simplify the stored objects. To investigate someday : in recordops, the RECMETHODS is storing some evar_maps. This is ok for the moment, but might not be in the future (cf previous commit on auto hints). This RECMETHODS was not detected by my earlier tests : not used in the stdlib ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14627 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-08Esubst: make types of substitutions & lifts privatepuech
Allows to be sure that we apply the smart constructors. Propagate the change to Closure, Reduction, Term, Cbv and Newring git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14386 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-04moins de reification inutile, noatations standardspottier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14385 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Newring: generic = on constr replaced by eq_constrpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14372 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29replaced some generic = on constr by eq_constrpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14364 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Newring: replaced some generic = on constr by eq_constrpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14356 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Newring: replaced generic = on constr by eq_constrpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14351 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Newring: generic Pervasives.compare on constr replaced by constr_ordpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14347 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Newring: generic equality on constr replaced by constr_equalpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14343 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-26Integral domainspottier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14299 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-26Ring2 devient Ncring et la reification par les type classes est partageepottier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14298 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-28Some cleanup of Zdiv and Zquot, deletion of useless Zdiv_defletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14244 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-21Follow-up concerning eqb / ltb / leb comparisonsletouzey
- All statement using reflect are made transparent. (Otherwise, since reflect isn't in Prop, extraction complains now about opaque Type definition). - remove two local Peqb_spec and Neqb_spec, now provided globally as Pos.eqb_spec and N.eqb_spec. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14232 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-10ring2, cring, nsatz avec type classe avec parametres plus notationspottier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14175 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 17:20:50 +0000