aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Dont recompute the contents of the proof window when entering theGravatar vgross2010-04-28
| | | | | | cursor. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12968 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #2245, incorrect handling of Context in sections inside moduleGravatar msozeau2010-04-27
| | | | | | | types. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12967 85f007b7-540e-0410-9357-904b9bb8a0f7
* small detail about Scheme Equality Gravatar vsiles2010-04-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12966 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a new exception for already declared Schemes, Gravatar vsiles2010-04-27
| | | | | | | | | so that we can return the right error message when trying to declare a scheme twice. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12965 85f007b7-540e-0410-9357-904b9bb8a0f7
* Misc small fixes : warning, dep cycles, ocamlbuild...Gravatar letouzey2010-04-26
| | | | | | | | | | | | - git ignore g_decl_mode.ml - exhaustive match for pp_vernac (BeginSubproof, ...) - for ocamlbuild, remove a spurious cycle in recordops.mli (unnecessary open of Classops), and fixes of *.itargets and _tags The compilation via ocamlbuild still need some work, since plugin firstorder now depends on the new plugin decl_mode git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12964 85f007b7-540e-0410-9357-904b9bb8a0f7
* Disable ideal-features tests by defaultGravatar glondu2010-04-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12963 85f007b7-540e-0410-9357-904b9bb8a0f7
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a fairly large commit (around 140 files and 7000 lines of code impacted), it will cause some troubles for sure (I've listed the know regressions below, there is bound to be more). At this state of developpement it brings few features to the user, as the old tactics were ported with no change. Changes are on the side of the developer mostly. Here comes a list of the major changes. I will stay brief, but the code is hopefully well documented so that it is reasonably easy to infer the details from it. Feature developer-side: * Primitives for a "real" refine tactic (generating a goal for each evar). * Abstract type of tactics, goals and proofs * Tactics can act on several goals (formally all the focused goals). An interesting consequence of this is that the tactical (. ; [ . | ... ]) can be separated in two tacticals (. ; .) and ( [ . | ... ] ) (although there is a conflict for this particular syntax). We can also imagine a tactic to reorder the goals. * Possibility for a tactic to pass a value to following tactics (a typical example is an intro function which tells the following tactics which name it introduced). * backtracking primitives for tactics (it is now possible to implement a tactical '+' with (a+b);c equivalent to (a;c+b;c) (itself equivalent to (a;c||b;c)). This is a valuable tool to implement tactics like "auto" without nowing of the implementation of tactics. * A notion of proof modes, which allows to dynamically change the parser for tactics. It is controlled at user level with the keywords Set Default Proof Mode (this is the proof mode which is loaded at the start of each proof) and Proof Mode (switches the proof mode of the current proof) to control them. * A new primitive Evd.fold_undefined which operates like an Evd.fold, except it only goes through the evars whose body is Evar_empty. This is a common operation throughout the code, some of the fold-and-test-if-empty occurences have been replaced by fold_undefined. For now, it is only implemented as a fold-and-test, but we expect to have some optimisations coming some day, as there can be a lot of evars in an evar_map with this new implementation (I've observed a couple of thousands), whereas there are rarely more than a dozen undefined ones. Folding being a linear operation, this might result in a significant speed-up. * The declarative mode has been moved into the plugins. This is made possible by the proof mode feature. I tried to document it so that it can serve as a tutorial for a tactic mode plugin. Features user-side: * Unfocus does not go back to the root of the proof if several Focus-s have been performed. It only goes back to the point where it was last focused. * experimental (non-documented) support of keywords BeginSubproof/EndSubproof: BeginSubproof focuses on first goal, one can unfocus only with EndSubproof, and only if the proof is completed for that goal. * experimental (non-documented) support for bullets ('+', '-' and '*') they act as hierarchical BeginSubproof/EndSubproof: First time one uses '+' (for instance) it focuses on first goal, when the subproof is completed, one can use '+' again which unfocuses and focuses on next first goal. Meanwhile, one cas use '*' (for instance) to focus more deeply. Known regressions: * The xml plugin had some functions related to proof trees. As the structure of proof changed significantly, they do not work anymore. * I do not know how to implement info or show script in this new engine. Actually I don't even know what they were suppose to actually mean in earlier versions either. I wager they would require some calm thinking before going back to work. * Declarative mode not entirely working (in particular proofs by induction need to be restored). * A bug in the inversion tactic (observed in some contributions) * A bug in Program (observed in some contributions) * Minor change in the 'old' type of tactics causing some contributions to fail. * Compilation time takes about 10-15% longer for unknown reasons (I suspect it might be linked to the fact that I don't perform any reduction at QED-s, and also to some linear operations on evar_map-s (see Evd.fold_undefined above)). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12961 85f007b7-540e-0410-9357-904b9bb8a0f7
* Applying François Garillot's patch (#2261 in bug tracker) for extendedGravatar herbelin2010-04-22
| | | | | | | syntax of "Implicit Type" (that can now be "Implicit Types" and can now accept several blocks of variables of a given type). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12960 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ignore *.stamp filesGravatar herbelin2010-04-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12959 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed bugs from commit 12954 on unification complexityGravatar herbelin2010-04-20
| | | | | | | | (two typos + failure to preserve the "natural" alias choice that was made in 8.2 in presence of definitions x:=y where y is inversible either as x or y, the latter being the "natural" choice). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12958 85f007b7-540e-0410-9357-904b9bb8a0f7
* missing space in error messageGravatar vsiles2010-04-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12957 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed bug #2999 (destruct was not refreshing universes of what it generalized *)Gravatar herbelin2010-04-20
| | | | | | | | + changed printing of universe Type(0) to Set, so not to show that the implementation starts numbering with Set=Type(0) while documentation uses Type(0) for the common type of Prop and Set. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12956 85f007b7-540e-0410-9357-904b9bb8a0f7
* Propagated fix to bug 2127 (Hint Rewrite badly globalized in modules) to 8.2Gravatar herbelin2010-04-20
| | | | | | (the bug was fixed for trunk/8.3 in revision 12354). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12955 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reduced the complexity of evar instantiations from O(n^3) to less than O(n^2).Gravatar herbelin2010-04-19
| | | | | | | | | | | | | | Reasoning modulo variable aliases induced an extra lookup in the environment at each inversion of the components of the evar instances: precomputing the aliases map allowed to gain a factor n. Moreover, solve_evar_evar_l2r was recomputing the evar substitution from the evar instance n more times than needed. Function solve_evar_evar_l2r is still on O(n^2) but it does not seem to be used so often actually. The trivial case has been optimized (linear time) but the general case could probably be also cut down to O(n*log(n)) if needed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12954 85f007b7-540e-0410-9357-904b9bb8a0f7
* In function "substitution_prefixed_by" the prefix test on module path Gravatar soubiran2010-04-19
| | | | | | | has been changed to a strict prefix test. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12952 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed some printing bugs.Gravatar herbelin2010-04-18
| | | | | | | | | | - Notations with coercions to funclass inserted were not working any longer since r11886. Made a fix but maybe should we eventually type the notations so that they have a canonical form (and in particular with coercions pre-inserted?). - Improved spacing management in printing extra tactic arguments "by" and "in". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12951 85f007b7-540e-0410-9357-904b9bb8a0f7
* A pass on the CHANGES file + credits for 8.3 (completing commit 12906Gravatar herbelin2010-04-17
| | | | | | | which involontarily propagated to the central repository a preliminary version of them). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12950 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moved Case3.v from ideal features to success (it works since 8.2).Gravatar herbelin2010-04-17
| | | | | | | | | Two other tests are still "ideal features" though not failing (evars_subst.v is a complexity test still of bad complexity and universes.v just describes an improvement to do without checking anything). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12949 85f007b7-540e-0410-9357-904b9bb8a0f7
* Solved a few problems of auto by bypassing the call to apply.Gravatar herbelin2010-04-17
| | | | | | | | | | | | Indeed, calling apply was inefficient (doing again a unification known to work) and moreover unsound (apply's unification is poorly tunable and the flags used in the first unification - in clenv_unique_resolve - were lost for apply). Solved the problem of still having a pretty acceptable user-friendly "info auto" by concealing the direct call to "clenv_refine" as a call to apply. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12948 85f007b7-540e-0410-9357-904b9bb8a0f7
* Use nice "unfold" instead of ugly "change" to display calls to unfold hintsGravatar herbelin2010-04-17
| | | | | | in "info auto". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12947 85f007b7-540e-0410-9357-904b9bb8a0f7
* cf. 12945Gravatar soubiran2010-04-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12946 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: cosmetics when using ocaml + Extract Inductive to symbolsGravatar letouzey2010-04-16
| | | | | | | | | | | - When using an infix constructor such as (::), whitespaces are to be given by the user, for instance Extract Inductive list => list [ "[]" "( :: )" ]. - Remove ugly whitespaces when using the ""-for-Pair trick: Extract Inductive prod => "(*)" [ "" ]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12944 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: restore (temporarily?) a very limited form of linear letin reductionGravatar letouzey2010-04-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12943 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: less eta in calls to global functions, better optimization phaseGravatar letouzey2010-04-16
| | | | | | | | | | | | - we saturate the normalize function : as long as (kill_dummy + simpl) isn't a nop, we do it again. - generalize_case allowed on all types of theories/Init/*.v instead of only bool,sumbool,sumor. NB: this optim cannot be performed on any type, it might produce untyped code. - common_branch allowed on match with one branch: in this situation it indicates whether the match can be removed or not. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12942 85f007b7-540e-0410-9357-904b9bb8a0f7
* Names.mli: double declaration of mind_modpathGravatar letouzey2010-04-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12941 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: improvement of optimizations (kill_dummy, optim_fix)Gravatar letouzey2010-04-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12940 85f007b7-540e-0410-9357-904b9bb8a0f7
* Util: remove list_split_at which is a clone of list_chopGravatar letouzey2010-04-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12939 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: ad-hoc identifier type with annotations for reductionsGravatar letouzey2010-04-16
| | | | | | | | | | | | | | | | * An inductive constructor Dummy instead of a constant dummy_name * The Tmp constructor indicates that the corresponding MLlam or MLletin is extraction-specific and can be reduced if possible * When inlining a glob (for instance a recursor), we tag some lambdas as reducible. In (nat_rect Fo Fs n), the head lams of Fo and Fs are treated this way, in order for the recursive call inside nat_rect to be correctly pushed as deeper as possible. * This way, we can stop allowing by default linear beta/let reduction even under binders (can be activated back via Set Extraction Flag). * Btw, fix the strange definition of non_stricts for (x y). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12938 85f007b7-540e-0410-9357-904b9bb8a0f7
* Compare_dec : a few better proofs (and extracted terms), some more DefinedGravatar letouzey2010-04-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12937 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: less _ in Haskell (typically for False_rect), less toplevel ↵Gravatar letouzey2010-04-16
| | | | | | eta-expansions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12936 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing redundant internal variants of apply tactic and simplification of ↵Gravatar herbelin2010-04-14
| | | | | | | | ML names (late consequences of commit r12603) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12934 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove only *.v.log files in clean of test-suite/MakefileGravatar glondu2010-04-13
| | | | | | ...so that "./check > check.log" works as expected. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12933 85f007b7-540e-0410-9357-904b9bb8a0f7
* Look for csdp in $PATH at runtime, remove -csdpdir configure optionGravatar glondu2010-04-11
| | | | | | | | | The csdp path computed by the configure script wasn't used at all, but was forcing presence of csdp at configure time whereas it is not used at all in the build process. Instead, we replace the configure-time check with a runtime check for existence of csdp in $PATH. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12929 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove unused functions run_sdpaGravatar glondu2010-04-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12928 85f007b7-540e-0410-9357-904b9bb8a0f7
* Recovering 8.2 behavior of "simple (e)apply" (and hence of "(e)auto").Gravatar herbelin2010-04-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12927 85f007b7-540e-0410-9357-904b9bb8a0f7
* Run parallelized test-suite in "check" target of main MakefileGravatar glondu2010-04-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12926 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prettier test-suite/MakefileGravatar glondu2010-04-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12925 85f007b7-540e-0410-9357-904b9bb8a0f7
* Optimized need for delimiters when disjoint scopes for strings andGravatar herbelin2010-04-10
| | | | | | numerals are open (see e.g. part of bug report #2044). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12924 85f007b7-540e-0410-9357-904b9bb8a0f7
* Update .gitignoreGravatar glondu2010-04-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12923 85f007b7-540e-0410-9357-904b9bb8a0f7
* Use the Makefile in test-suite/checkGravatar glondu2010-04-10
| | | | | | | | The output format is preserved, but not the dynamics (results are showed all at once at the end). This script could be removed altogether once the main Makefile (and daily bench) are fixed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12922 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile for the test-suiteGravatar glondu2010-04-10
| | | | | | | | | | | | | | | Using a Makefile for tests allows (easily) running them in parallel, running and/or benching a single one, adding depedencies between them, and running them with a version of Coq different than the one compiled with the current source tree. The new way to make statistics about successes/failures is also more reliable (I found bugs in the previous one). Statistics (on AMD Phenom(tm) 9950 Quad-Core Processor 2.6 GHz): - plain sh script: ~ 3 min - make -j6: ~ 1 min git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12921 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix typos in test-suite scriptGravatar glondu2010-04-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12920 85f007b7-540e-0410-9357-904b9bb8a0f7
* Granting wish #2229 (InA_dec transparent) and Michael Day's coq-clubGravatar herbelin2010-04-10
| | | | | | 8 April 2010 wish (addition of map_eq_nil). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12919 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test for bug #2231 (unexpected error when using let/if over an inductiveGravatar herbelin2010-04-10
| | | | | | parameter in the type of a constructor). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12918 85f007b7-540e-0410-9357-904b9bb8a0f7
* Partially fixed bug #2231 (an inductive parameter name was internallyGravatar herbelin2010-04-10
| | | | | | | | | | | | used as a binding name in the return predicate of a Let/If case analysis causing a surprising error message; solved the problem by not checking for this kind of internal variables when the return predicate is anyway not given by the user; ideally, it should be detected that in the arguments of the inductive type, the parameter names can be reused w/o provoking captures - which are bad if the argument is implicit). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12917 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing various coqdep bugs (#2118, #2242, #2274)Gravatar herbelin2010-04-10
| | | | | | | | | | | | | - Made resolution of clashing -I options consistent with coqc (bug #2242) - Made semantics of -R consistent with the one introduced by revision 11188 in coqc, i.e. -R now makes visible all intermediate qualification levels (bug #2274) - Added support for -I -as and -R -as syntax - Extended escaping of special chars of GNU make and used escaping more systematically (bug #2118) - Made warnings follow English typography git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12916 85f007b7-540e-0410-9357-904b9bb8a0f7
* Change definition of FSetList so that equality is LeibnizGravatar glondu2010-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12913 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add test-suite/lia.cache to .gitignoreGravatar glondu2010-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12912 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing part 1 of bug #2242 (-I -as and -R -as were supported forGravatar herbelin2010-04-09
| | | | | | coqtop but not coqc). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12911 85f007b7-540e-0410-9357-904b9bb8a0f7
* Granting wish #2249 (checking existing lemma name also when in a section).Gravatar herbelin2010-04-09
| | | | | | Simplified in passing generation of names for the "Goal" command. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12910 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 18:29:56 +0000