aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2009-12-17ZOdiv: fully use generic properties from ZDivTrunc.vletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12596 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-17Reverse order of arguments in min_case_strong for better uniformity (and ↵letouzey
compatibility...) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12595 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-17Division in Numbers : more properties, new filenames based on a paper by R. ↵letouzey
Boute Following R. Boute (paper "the Euclidean Definition of the Functions div and mod"): - ZDivFloor.v for Coq historical division (former ZDivCoq.v) - ZDivTrunc.v for Ocaml convention (former ZDivOcaml.v) - ZDivEucl.v for "Mathematical" convention 0<=r (former ZDivMath.v) These property functors are more or less finished (except that sign and abs stuff should be migrated to a separate file). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12594 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-16correction de la nouvelle option pour functional inductionjforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12593 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-16adding an option functional_induction_rewrite_dependent to make functional ↵jforest
induction using not v8.2 version of subst. By default functional induction uses new version of subst git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12592 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-16Division in Numbers: more properties proved (still W.I.P.)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12591 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-15A generic euclidean division in Numbers (Still Work-In-Progress)letouzey
- For Z, we propose 3 conventions for the sign of the remainder... - Instanciation for nat in NPeano. - Beginning of instanciation in ZOdiv. Still many proofs to finish, etc, etc, but soon we will have a decent properties database for all divisions of all instances of Numbers (e.g. BigZ). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12590 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-15file integrated into the archive by mistakeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12589 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-15Description of the new features of the module system (part two).soubiran
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12588 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-15Description of the new features of the module system (first part).soubiran
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12587 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-14Improved strategy for rewriting lemma possibly depending because of evars.herbelin
Explained in CHANGES how to cope with the change of semantics of abbreviations wrt implicit arguments positions propagation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12586 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-13Addition of mergesort + cleaning of the Sorting libraryherbelin
- New (modular) mergesort purely using structural recursion - Move of the (complex) notion of permutation up to setoid equality formerly defined in Permutation.v to file PermutSetoid.v - Re-use of the file Permutation.v for making the canonical notion of permutation that was in List.v more visible - New file Sorted.v that contains two definitions of sorted: "Sorted" is a renaming of "sort" that was defined in file Sorting.v and "StronglySorted" is the intuitive notion of sorted (there is also LocallySorted which is a variant of Sorted) - File Sorting.v is replaced by a call to the main Require of the directory - The merge function whose specification rely on counting elements is moved to Heap.v and both are stamped deprecated (the sort defined in Heap.v has complexity n^2 in worst case) - Added some new naming conventions - Removed uselessly-maximal implicit arguments of Forall2 predicate git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12585 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-13Made the side-conditions of lemmas always come last when chaining "apply in"herbelin
in presence of destruction of conjunctive types. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12584 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-13Completion of r12580 (better rendering of dependent rewrite and inversion).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12583 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-13Deactivating printing of {| |} for records when option Printing All is set.herbelin
Simplifying the printing of "in" clause keeping the same defaults as in parsing (e.g. "simpl" is printed "simpl" and not "simpl in *"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12582 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-13Fixing bug in printing option as of remember and generalizeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12581 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-13Revision 12557 continued (better rendering of dependent rewrite)herbelin
(expected goal was not correct for rewriting in hypotheses) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12580 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-12Fixed incorrect computation of possible guard in presence of `{ ... } contexts.herbelin
Also removed used of local_binders_length and local_assums_length which are now incorrect due to the possible presence of `{ ... } contexts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12579 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-12Updated compatibility for rewriting equality proofs that are dependentherbelin
- made the new "subst'" the default by renaming it "subst"; - renamed old "subst" into "simple subst"; - add option for non-rewriting of dependent proofs in general_rewrite and co - kept use of dependent proofs in the "subst" call of "functional induction", in spite it introduced incompatibilities (in Compcert). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12578 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-12Improved the rendering of "dependent rewrite" and hence of "inversion"herbelin
by contracting in advance the projT (existT ...) redexes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12577 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 10:28:12 +0000