aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2009-12-11Deport the backtracking code out of the idevgross
Backtracking code now lies entirely into ide/coq.ml. Datatypes have been tweaked to easen the separation to come. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12576 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-10NZDomain: investigation of the shape of NZ domain, more results about ↵letouzey
ofnat:nat->NZ.t git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12575 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-09Factorisation between Makefile and ocamlbuild systems : .vo to compile are ↵letouzey
in */*/vo.itarget On the way: no more -fsets (yes|no) and -reals (yes|no) option of configure if you want a partial build, make a specific rule such as theories-light Beware: these vo.itarget should not contain comments. Even if this is legal for ocamlbuild, the $(shell cat ...) we do in Makefile can't accept that. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12574 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-08Migration of ProtectedToplevel and Line_oriented_parser into new contrib ↵letouzey
Interface the ProtectedLoop feature was used only by CoqInterface. Idem for stuff in Line_oriented_parser git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12573 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-08Fix the build of coq via ocamlbuildletouzey
- no more plugins/interface - a few missing files in theories.itarget - a few things required Unix now git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12572 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-08integrate MSetToFiniteSet into the compilation (and fix it)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12571 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-08Sos.ml: no more warningsletouzey
apart for a few non-exhaustive patterns, there was also some unused let-in variables. Hard to check whether the apparently useless code is doing some side-effect or not... It seems not, so I've removed completely the corresponding code. Frederic, is that ok ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12570 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-08Declaremods.ml: a useless function wrongly introduced in last commitletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12569 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-07Fix bug #2197 (option show_toolbar not taken into account at startup)vgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12568 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-07Remove the "detach script windows" feature.vgross
See bug #2173. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12567 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-07No more specific syntax "Include Self" for inclusion of partially-applied ↵letouzey
functors For Module F(X:SIG), making now a Include F will try to find the X fields in the current context, just as was doing earlier Include Self F. This specific syntax is removed, freeing the keyword "Self". Anyway, with the use of the syntax "<+" there was already hardly any need for syntax "Include Self". Idem for Include Type. Beware that a typo such as "Include F" instead of "Include F G" will produce a different message now, about a missing field instead of a not-enough-applied functor. By the way, some code clean-up and factorisation of inner recursive functions in declaremods.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12566 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-07revert on commit r12553barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12565 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-06Turn evars created by a tactic application into a subgoal immediately inmsozeau
typeclass resolution. Makes the backtracking heuristic correct again and avoids "late" backtracking on an unsolvable existential. Compilation time is back to normal. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12564 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-06Forgot a file in last commit.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12563 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-06Fix anomaly when using typeclass resolution with filtered hyps in evars.msozeau
Make setoid_rewrite-through-rewrite's selection of occurences more robust: do not try unification with reduction if not needed. This changes a few scripts that were using reduction in a far from obvious way and could break more. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12562 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-03Still continuing r12485-12486, r12549, r12556 (cleaning around name generation)herbelin
Removed one more bug in simplification of visibly_occur_id in r12549 + improved CHANGES message git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12561 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-03Restored rewriting of JMeq using JMeq_rect and co when the domains are the sameherbelin
(this was lost since revision 12481). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12560 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-03Fix bug #2191 : Serious "undo" performance degradation since 8.2pl1vgross
This reverts commit 12537 This reverts commit 12199 This reverts commit 12198 This reverts commit 12172 (introduced the bug) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12559 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-03declaremods.ml <--- code factoringsoubiran
mod_subst <--- Some inlining informations was propagated into module implementation whereas those informations should stay in module type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12558 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-03Rename proper to proper_prf to avoid clash with CoRN, msozeau
it's rarely used anyway. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12557 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-02Continuing r12485-12486 and r12549 (cleaning around name generation)herbelin
- fixed misunderstanding of the role of nenv while simplifying code of occur_id in namegen.ml, - documented the possible incompatibilites in CHANGES - fixed output/Naming.v test, and fixed the count of misc. tests in test-suite/check. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12556 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-02Remove interface pluginglondu
It has moved to the contribs (Sophia-Antipolis/Interface). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12555 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-02Update .gitignoreglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12554 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-01two improvements of the guard condition:barras
- a matched expression is reduced (in order to check if it's a subterm) to hnf only when it contains variables that are subterms; - a matched expression is checked to be a subterm only when it belongs to a *recursive* type. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12553 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-01fix coqchk options documentationbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12552 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-01install manpage of coqchkbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12551 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-01Fix make_exact_entry to allow applying [forall x, P x] hints directly,msozeau
avoiding the introduction of eta-redexes. Prioritize hints over intros in typeclass resolution to profit from that. Add a minor fix in coqdoc by F. Garillot. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12550 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-01Continuing r12485-12486 (cleaning around name generation)herbelin
- backtrack on incompatibility introduced in intro while trying to simplify the condition about when to restart the subscript of a name (the legacy says: find a new name from x0 if the name xN exists in the context but find a new name from xN+1 if the name xN does not exists in the context but is a global to avoid). - made the names chosen by "intro" compliant with the ones printed in the goal and used for "intros until" (possible source of rare incompatibilities) [replaced the use of visibly_occur_id for printing the goal into a call to next_name_away_in_goal] - also made the names internal to T in "T -> U" printed the same in the goal as they are while printing T after it is introducted in the hypotheses [non contravariant propagation of boolean isgoal in detype_binder] - simplified a bit visibly_occur_id (the Rel and Var cases were useless as soon as the avoid list contained the current env); still this function is costly with polynomial time in the depth of binders - see file output/Naming.v for examples git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12549 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-01Fix bug in typeclass resolution. Better handling of universes inmsozeau
the generalization tactic. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12548 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-30Fix backtracking heuristic in typeclass resolution. msozeau
Now that backtracking is working correctly, we need to avoid a non-termination issue introduced by the [RelCompFun] definition in RelationPairs, by adding a [Measure] typeclass. It could be used to have a uniform notation for measures/interpretations in Numbers and be but in the interfaces too, only the mimimal change was implemented. Fix syntax change in test-suite scripts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12547 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-27Added support for definition of fixpoints using tactics.herbelin
Fixed some bugs in -beautify and robustness of {struct} clause. Note: I tried to make the Automatic Introduction mode on by default for version >= 8.3 but it is to complicated to adapt even in the standard library. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12546 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-27Substitute terms for evars-as-goals as soon as they are solved inmsozeau
typeclass resolution. Fixes a bug reported by Eelis van der Weegen. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12545 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-26svn:ignore propertyherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12544 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-26Fixing xml theory file export (was not consistent with coqdoc fileherbelin
naming heuristic). Added a corresponding test. Note: maybe should the generated .v file for exporting the theory be made of a valid ident if ever coqdoc eventually follows coq convention: currently it has name foo.theory.v which is not coqc-compilable. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12543 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-25Fix for notation scope & inductive typesvsiles
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12542 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-24Minor fixes in typeclasses, avoiding repeated evar normalizations.msozeau
Improve generalization by equalities tactic, now allowing to generalize an arbitrary application, e.g. in preparation for applying an elimination principle for a function. This adds a flag to generalize_dep so that it doesn't abstract the variable if it is defined, just introducing a let-in. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12541 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-24Small extra result on JMeq vs eq_dep.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12540 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-23Ergonomy and robustness fixvgross
Sentences are locked up to the period, and it's now possible to eval when there is no final whitespace. CoqIde will refuse to evaluate further if there is no whitespace, though. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12539 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-21Lazier behaviour of [auto] when introducing hypothesis: query the hint db's ↵puech
only when necessary. Hopefully should speed up [auto] a little. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12538 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-19Refactoring of coqide backtrack code, with the intent to put everythingvgross
into coqtop. Also, some cleaning in ide/gtk_parsing.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12537 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-19Correction du bug #2118 (Coqdep does not escape #)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12536 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-18Now "Include Self <expr>" handles partially applied functors, cf for example ↵soubiran
NZAddPropFunct in NZAdd.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12535 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-18Diamond-shape instead of linear hiearchy in Numbers/NatIntletouzey
NZBase -- NZAdd -- NZMul | | NZOrder ---------- NZAddOrder -- NZMulOrder -- NZProperties This is done by transforming NZBase into a functorial module type, and making NZAdd NZMul NZOrder accept an instance of NZBase as parameter. This is possible thanks to a combination of various new features of modules: - interactive proofs in module type (ie functors can be turned into type functors) - Include Type in Module (ie type functors can be turned into functors) - Include Self, <+ , etc, etc... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12534 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-18Allow interactive proofs in module typesletouzey
Elie suggested this change, it seems that there are no real reasons to forbid interactive proofs in module types. A functor can now be written with Module Type, and can hence be used later as parameter of other functors (while it can also be translated to regular functor by a Include Type in a Module). See next commit for a example of diamond-shape developpement that become possible with this feature. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12533 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-18Module subtyping : allow many <: and module type declaration with <:letouzey
Any place where <: was legal can now contain many <: declarations. Moreover we can say that the module type we are declaring is a subtype of an earlier module type. See DecidableType2 for examples. Also try to handle correctly the freeze/unfreeze summaries when simulating start/include/end (syntax ... := ... <+ ...) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12532 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-16New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))letouzey
"Module M (...) := M1 <+ M2 <+ M3 <+ ..." is now a shortcut for "Module M (...). Include M1. Include M2. Include M3... End M." Moreover M2,M3,etc can be functors as long as they find what they need in what comes before them (see new command "Include Self"). The only real constraint is that M1,M2,M3,... should not have common elements (for the moment (?)). Same behavior for signature : Module Type M := M1 <+ M2 <+ M3. Note that this <+ is _not_ a primitive construct of the module language, for instance it cannot be used in signature (Module M <: M1 <+ M2 is illegal for the moment). Some example of use in Decidable2 and NZAxioms git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12530 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-16Taking advantage of the new "Include Self Type" in DecidableType2 and NZAxiomsletouzey
We can now have a diamond-like approch to extentions of signatures, instead of a linear-only chains as earlier... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12529 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-16Include Self (Type) Foo: applying a (Type) Functor to the current contextletouzey
If you have some Module Type F (X:Sig), and you are in a Module Type containing everything required to satisfy Sig (typically thanks to some earlier Include), then you can say Include Self Type F, and voila, objects of F are now added in your context, instantiated by local objects. Same behavior (hopefully) for modules and functors when using Include Self F. This experimental new command allows to easily produce static signatures out of functorial ones: Module Type F_static. Include Sig. Include Self F. End F_static. ... is similar to ... Module Type F_static. Declare Module X:Sig. Include F X. End F_static. ... but without the pollution of this artificial inner module X. This allow to split things in many othogonal components, and then mix them. It is a lightweight way to tackle the "diamond problem" of modular developpements without things like "overlapping" Include's (planned, but not yet there). See next commit for an example of use. Thanks to Elie for the debugging of my first ugly prototype... NB: According to Yann R.G., this is related with Scala's Traits. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12528 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-16Some lemmas about dependent choice + extensions of Compare_dec +herbelin
synonyms in Le.v, Lt.v, Gt.v. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12527 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-15Fix type class discharge again.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12526 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 11:21:55 +0000