aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2009-10-29Fix flat_map definition so that it plays nicely with fixglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12444 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-29Fixed some typos in the reference manual.gmelquio
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12443 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-29Revision 12439 continued, printing part (notations to names behaveherbelin
like the name they refer to). Fixing buggy test-suite implicit.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12442 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-29Fix bug in dnet.ml, which missed some results when filtering one term ↵puech
against many patterns. Conflicts: lib/dnet.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12441 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-28Integrate a few improvements on typeclasses and Program from the equations ↵msozeau
branch and remove equations stuff which moves to a separate plugin. Classes: - Ability to define classes post-hoc from constants or inductive types. - Correctly rebuild the hint database associated to local hypotheses when they are changed by a [Hint Extern] in typeclass resolution. Tactics and proofs: - Change [revert] so that it keeps let-ins (but not [generalize]). - Various improvements to the [generalize_eqs] tactic to make it more robust and produce the smallest proof terms possible. Move [specialize_hypothesis] in tactics.ml as it goes hand in hand with [generalize_eqs]. - A few new general purpose tactics in Program.Tactics like [revert_until] - Make transitive closure well-foundedness proofs transparent. - More uniform testing for metas/evars in pretyping/unification.ml (might introduce a few changes in the contribs). Program: - Better sorting of dependencies in obligations. - Ability to start a Program definition from just a type and no obligations, automatically adding an obligation for this type. - In compilation of Program's well-founded definitions, make the functional a separate definition for easier reasoning. - Add a hint database for every Program populated by [Hint Unfold]s for every defined obligation constant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12440 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-28Made that notations to names behave like the names they refer to wrtherbelin
implicit arguments and scope (use Implicit Arguments or Arguments Scope commands instead if not the desired behaviour). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12439 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-28Fixed a bug when reporting unexisting reference to an inductiveherbelin
(introduced in r12323). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12438 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-28Clarification in commentsglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12437 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-28Remove old compatibility stuff (Tacred.nf)glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12436 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-28Make usage of Dyn explicitglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12435 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-28Backport fix for indexing of sorts which collapse every Type occurrencemsozeau
into a SortLabel None. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12434 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-28Typo in the refmanpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12433 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-28Fix incorrect registration of objects in libtypes.ml when defining a module.puech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12432 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-28Same as commit 12430 but with the good version of the function iter_all_segmentsoubiran
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12431 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-28From now SearchAbout requests search also inside INCLUDE libobject.soubiran
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12430 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-28Module type expressions of the form (Fsig X) with Definition foo := bar are ↵soubiran
now accepted. +svn:ignore property on folders git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12429 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-27Add a new vernacular command for controling implicit generalization ofmsozeau
variables with syntax: [Local?|Global] Generalizable Variable(s)? [all|none|id1 idn]. By default no variable is generalizable, so this patch breaks backward compatibility with files that used implicit generalization (through Instance declarations for example). To get back the old behavior, one just needs to use [Global Generalizable Variables all]. Make coq_makefile more robust using [mkdir -p]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12428 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-27Fixes around typeclasses:msozeau
- Correct discharge/classify/rebuild for instances. Semantic of Global/Local: local by default in sections, global by default in modules. - Fix the discrimination net's handling of type universes, let the unification do it. - Correct the typeclass resolution tactic so that when extern tactics themselves launch class resolution we don't duplicate work. Problem reported by Arthur Chargueraud. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12427 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-27Added option --external to coqdoc to bind an url to an external library.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12426 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-27Documentation of the Local and Global modifiers.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12425 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-27fix previous commitcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12424 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-27fixed czar bug with parametric inductivescorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12423 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-26Fix Setoid documentation.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12421 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-26Local/Global revision 12418 continuedherbelin
- Fixing non-export of newly created Local Argument Scope. - Fixing bad discharge of local variables in nested sections (bug still exists in v8.2). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12420 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-26Adapted test unfold.v after eq gets its argument maximally insertedherbelin
(commit r12379). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12419 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-26New cleaning phase of the Local/Global option managementherbelin
- Clarification and documentation of the different styles of Local/Global modifiers in vernacexpr.ml - Addition of Global in sections for Open/Close Scope. - Addition of Local for Ltac when not in sections. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12418 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-26New functors for gmap and gset.soubiran
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12417 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-25Restore (and test) broken chaining of lemmas in "apply in" in presenceherbelin
of side conditions. Fix a small presentation issue in printing the "exists" tactic. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12416 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-25fixed bug in Czar grammarcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12415 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-25Add support for remaining side-conditions in "apply in as".herbelin
Tolerate that the place where to move an hypothesis with destruct is not "safe" if the lemma has dependent parameters inferred lately. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12412 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-25Improved the treatment of Local/Global options (noneffective Local onherbelin
Implicit Arguments, Arguments Scope and Coercion fixed, noneffective Global in sections for Hints and Notation detected). Misc. improvements (comments + interpretation of Hint Constructors + dev printer for hint_db). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12411 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-24Fixing XML doc (COQ_XML not working as an environment variable).herbelin
Fixing English grammar in inversion error message (reported in bug #2164). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12409 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-23First debug... the renaming of librairies was not working and auto/dn were ↵soubiran
not taking in account equivalent names of inductive types. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12408 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-22Fix new instances that could easily make class resolution loop on msozeau
unconstrained goals (e.g. PreOrder A ?). Allow the unconstrained use of [proper_reflexive] again. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12407 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-21This big commit addresses two problems:soubiran
1- Management of the name-space in a modular development / sharing of non-logical objects. 2- Performance of atomic module operations (adding a module to the environment, subtyping ...). 1- There are 3 module constructions which derive equalities on fields from a module to another: Let P be a module path and foo a field of P Module M := P. Module M. Include P. ... End M. Declare Module K : S with Module M := P. In this 3 cases we don't want to be bothered by the duplication of names. Of course, M.foo delta reduce to P.foo but many non-logical features of coq do not work modulo conversion (they use eq_constr or constr_pat object). To engender a transparent name-space (ie using P.foo or M.foo is the same thing) we quotient the name-space by the equivalence relation on names induced by the 3 constructions above. To implement this, the types constant and mutual_inductive are now couples of kernel_names. The first projection correspond to the name used by the user and the second projection to the canonical name, for example the internal name of M.foo is (M.foo,P.foo). So: ************************************************************************************* * Use the eq_(con,mind,constructor,gr,egr...) function and not = on names values * ************************************************************************************* Map and Set indexed on names are ordered on user name for the kernel side and on canonical name outside. Thus we have sharing of notation, hints... for free (also for a posteriori declaration of them, ex: a notation on M.foo will be avaible on P.foo). If you want to use this, use the appropriate compare function defined in name.ml or libnames.ml. 2- No more time explosion (i hoppe) when using modules i have re-implemented atomic module operations so that they are all linear in the size of the module. We also have no more unique identifier (internal module names) for modules, it is now based on a section_path like mechanism => we have less substitutions to perform at require, module closing and subtyping but we pre-compute more information hence if we instanciate several functors then we have bigger vo. Last thing, the checker will not work well on vo(s) that contains one of the 3 constructions above, i will work on it soon... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12406 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-21MSetInterface: some explicit types to avoid Raw.t-instead-of-t effectletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12405 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-20Repaired bug #2165 (buggy coq example in Tactic Examples doc chapter)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12404 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-20Added syntactic coloration for 'Function'.gmelquio
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12403 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-20FSetCompat: a compatibility wrapper between FSets and MSetsletouzey
Thanks to the functors in FSetCompat, the three implementations of FSets (FSetWeakList, FSetList, FSetAVL) are just made of a few lines adapting the corresponding MSets implementation to the old interface. This approach breaks FSetFullAVL. Since this file is of little use for stdlib users, we migrate it into contrib Orsay/FSets. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12402 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-19Merge SetoidList2 into SetoidList: forgotten reference to the removed fileletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12401 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-19Merge SetoidList2 into SetoidList.letouzey
This file contains low-level stuff for FSets/FMaps. Switching it to the new version (the one using Equivalence and so on instead of eq_refl/eq_sym/eq_trans and so on) only leads to a few changes in FSets/FMaps that are minor and probably invisible to standard users. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12400 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-17Fixed a notation bug when extending binder_constr with empty levelsherbelin
(see Notations.v). Improved the "already occurs in a different scope" test and message. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12399 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-16OrderedType2 : trivial lemmas are turned into tests for order.letouzey
In particular we remove them from the hint db, a few autos become calls to order. Moreover, lt_antirefl --> lt_irrefl for uniformity. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12398 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-16Structure/OrderTac.v : highlight the "order" tactic by isolating it from ↵letouzey
FSets, and improve it As soon as you have a eq, a lt and a le (that may be lt\/eq, or (complement (flip (lt))) and a few basic properties over them, you can instantiate functor MakeOrderTac and gain an "order" tactic. See comments in the file for the scope of this tactic. NB: order doesn't call auto anymore. It only searches for a contradiction in the current set of (in)equalities (after the goal was optionally turned into hyp by double negation). Thanks to S. Lescuyer for his suggestions about this tactic. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12397 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-16note for later : when the tag table is shared, never, ever create twovgross
tags with the same name. This fixes file opening. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12396 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-15typo in doc of Extraction Blacklistletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12394 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-15MSetInterface: (W)Raw2Sets splitted in 2 (helps a future commit by Elie)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12393 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-15OrderedType2.order is slightly weaker since last commit, adapt accordinglyletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12392 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-15OrderedType2.order : fix the last fix (a fail at the wrong place)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12391 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-15Fix bug in typeclass resolution discoverd by Eeelis van der Weegen:msozeau
the wrong evar_defs was used when checking if an evar was to be resolved or not. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12390 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 17:02:03 +0000