aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Dag data structureGravatar gareuselesinge2013-08-08
| | | | | | | This is a very simple, only growing, Dag structure with per node optional info and per edge info git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16671 85f007b7-540e-0410-9357-904b9bb8a0f7
* Searchable stack data structureGravatar gareuselesinge2013-08-08
| | | | | | It is like Stack but one can search without popping git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16670 85f007b7-540e-0410-9357-904b9bb8a0f7
* Future library to represent pure computationsGravatar gareuselesinge2013-08-08
| | | | | | | | | | | | | Since the whole system is imperative, futures are run protecting the global state, and the final state is also saved to let the user freely chain futures. Futures can represent local (lazy) computations or remote ones (delegated). Delegating a future lets a third party assign its value at some poit in the future; in the meanwhile accessing the future value raises an exception. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16669 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing a warning in CoqIDE compilation.Gravatar ppedrot2013-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16668 85f007b7-540e-0410-9357-904b9bb8a0f7
* Small fix in IStream interface.Gravatar ppedrot2013-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16667 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing association lists in Constrintern.Gravatar ppedrot2013-08-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16666 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added more flags choice in desambiguating printer. The code isGravatar ppedrot2013-08-06
| | | | | | parametric on the list of possible flags. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16665 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tentative fix for bug #2961. When we have to print two terms thatGravatar ppedrot2013-08-05
| | | | | | | | | | | | | | | | | should be different, we compute the externalized form for both in the current state. If ever they coincide, we do it again with the implicit arguments flag set. In other words, if those two terms appear the same, we automatically print them with the implicit arguments flag on. This is a bit raw, and we may try other externalization flags, but I assume it to be (almost) sufficient for now. TODO: check every place where we could need such a feature, and try other flags. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16664 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added test for bug #2846.Gravatar ppedrot2013-08-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16663 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing #2846: Uncaught exception Reduction.NotArity.Gravatar ppedrot2013-08-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16662 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a test for bug #3062.Gravatar ppedrot2013-08-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16661 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing #3062. Computation of the value of a fresh identifier wasGravatar ppedrot2013-08-04
| | | | | | done too early and lead to dynamic conflicts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16660 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing useless casts between arrays and lists.Gravatar ppedrot2013-08-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16659 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing now useless merging primitives from Evd.Gravatar ppedrot2013-08-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16658 85f007b7-540e-0410-9357-904b9bb8a0f7
* Small cleaning of printing coercion failures in Ltac interpretation.Gravatar ppedrot2013-08-04
| | | | | | Now we at least print the type of the offending object. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16657 85f007b7-540e-0410-9357-904b9bb8a0f7
* Small fixes due to the arrival of OCaml 3.12.Gravatar ppedrot2013-08-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16656 85f007b7-540e-0410-9357-904b9bb8a0f7
* Replacing uses of association lists by maps in notations.Gravatar ppedrot2013-08-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16655 85f007b7-540e-0410-9357-904b9bb8a0f7
* Replacing an association list by a map in globalizing environment.Gravatar ppedrot2013-08-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16654 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding a dependent version of equal_f, thus fixing #3074.Gravatar ppedrot2013-08-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16653 85f007b7-540e-0410-9357-904b9bb8a0f7
* Small typo in Print Debug GCGravatar ppedrot2013-08-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16652 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a Print Debug GC command that displays the current state ofGravatar ppedrot2013-08-01
| | | | | | the OCaml GC, as indicated by [Gc.stat]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16651 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a test for bug #3088.Gravatar ppedrot2013-08-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16650 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing #3088. Translation from globconstrs to patterns was forgettingGravatar ppedrot2013-08-01
| | | | | | to register bound variables as such in the return clause. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16649 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documenting the Remove Hints command.Gravatar ppedrot2013-08-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16648 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added printing of instance priority to the Print Instances command.Gravatar ppedrot2013-08-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16647 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documenting the previous commit: Existing Instance with priority.Gravatar ppedrot2013-08-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16646 85f007b7-540e-0410-9357-904b9bb8a0f7
* Granting bug #3098: adding priority to Existing Instances.Gravatar ppedrot2013-08-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16645 85f007b7-540e-0410-9357-904b9bb8a0f7
* Typo in definition clos_reflGravatar ppedrot2013-07-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16644 85f007b7-540e-0410-9357-904b9bb8a0f7
* Granting wish #1781:Gravatar ppedrot2013-07-30
| | | | | | Parenthesis matching on click in all term displays. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16643 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tentative fix for #3054: we refresh universes in a term generatedGravatar ppedrot2013-07-29
| | | | | | | by congruence, as it seems to be done methodically on the remaining of this plugin. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16642 85f007b7-540e-0410-9357-904b9bb8a0f7
* better error message for unexpected renaming (closes #2987)Gravatar gareuselesinge2013-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16641 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revert "Only arguments declared as implicit can be renamed"Gravatar gareuselesinge2013-07-29
| | | | | | This reverts commit 18a89c271d540d794d44e41f50587bb1cad69802. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16640 85f007b7-540e-0410-9357-904b9bb8a0f7
* Protecting every call to current_term in CoqIDE so that callbackGravatar ppedrot2013-07-27
| | | | | | will not raise an exception if there is no opened tab. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16637 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a way to change dynamically coqtop arguments in CoqIDE.Gravatar ppedrot2013-07-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16636 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing #3089. This implied tweaking the definition of the lexicographicGravatar ppedrot2013-07-26
| | | | | | | | product of lists, hence possibly introducing incompatibilities. Parts of the patch by Chantal Keller. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16635 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bug #3093 by adding the asked test case.Gravatar ppedrot2013-07-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16634 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a concat function to List theory. Strangely, it was missing.Gravatar ppedrot2013-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16633 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fix uncaught exception NotASort from reductionops, moving decomp_sort to ↵Gravatar msozeau2013-07-19
| | | | | | | | | | retyping.ml - In unification's w_merge, assign the evars in the same order they were found. Might create rare incompatibilities. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16632 85f007b7-540e-0410-9357-904b9bb8a0f7
* "Boolean Equality" and "Case Analysis" are already off by default...Gravatar letouzey2013-07-17
| | | | | | ... no need to Unset them manually git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16631 85f007b7-540e-0410-9357-904b9bb8a0f7
* Declaremods: major refactoring, stop duplicating libobjects in modulesGravatar letouzey2013-07-17
| | | | | | | | | | | | | | | | | | | | | | | When refering to a module / module type, or when doing an include, we do not duplicate and substitution original libobjects immediatly. Instead, we store the module path, plus a substitution. The libobjects are retrieved later from this module path and substituted, typically during a Require. This allows to vastly decrease vo size (up to 50% on some files in the stdlib). More work is done during load (some substitutions), but the extra time overhead appears to be negligible. Beware: all subst_function operations should now be environment-insensitive, since they may be arbitrarily delayed. Apparently only subst_arguments_scope had to be adapted. A few more remarks: - Increased code factorisation between modules and modtypes - Many errors and anomaly are now assert - One hack : brutal access of inner parts of module types (cf handle_missing_substobjs) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16630 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modops.destr_functor without useless envGravatar letouzey2013-07-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16629 85f007b7-540e-0410-9357-904b9bb8a0f7
* Safe_typing: minor factorisationGravatar letouzey2013-07-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16628 85f007b7-540e-0410-9357-904b9bb8a0f7
* Lib.contents () instead of Lib.contents_after NoneGravatar letouzey2013-07-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16627 85f007b7-540e-0410-9357-904b9bb8a0f7
* More dynamic argument scopesGravatar letouzey2013-07-17
| | | | | | | | | | | | | | | | | | | | When arguments scopes are set manually, nothing new, they stay as they are (until maybe another Arguments invocation). But when argument scopes are computed out of the argument type and the Bind Scope information, this kind of scope is now dynamic: a later Bind Scope will be able to impact the scopes of an earlier constant. For Instance: Definition f (n:nat) := n. About f. (* Argument scope is [nat_scope] *) Bind Scope other_scope with nat. About f. (* Argument scope is [other_scope] *) This allows to get rid of hacks for modifying scopes during functor applications. Moreover, the subst_arguments_scope is now environment-insensitive (needed for forthcoming changes in declaremods). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16626 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction : message about lack of support for toplevel IncludeGravatar letouzey2013-07-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16625 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pre-create typeclass_instances and rewrite hintdb in AutoGravatar letouzey2013-07-17
| | | | | | | | | | | This way, we avoid relying on the add_auto_init hook. This hook is left for the moment, but could probably be removed someday. We also stop using create_hint_db, which has an effect on the libstack. This wasn't a problem per se, but could if init_summaries is used more (for instance to temporary reset coq). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16624 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a Register Inline command for the native compiler. Will be ported to ↵Gravatar mdenes2013-07-10
| | | | | | | | | | the VM too. Almost only a new grammar entry since the inlining machinery was already implemented. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16623 85f007b7-540e-0410-9357-904b9bb8a0f7
* Continuing r16621 on injection intro-patterns:Gravatar herbelin2013-07-10
| | | | | | | | - order of hypothesis was (historically) from right to left in injection but already from left to right in decomp_eq, so no need ro fix it there - made test Injection.v consistent with implementation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16622 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revising r16550 about providing intro patterns for applying injection:Gravatar herbelin2013-07-09
| | | | | | | | | | | | - Introduction of a specific notation for injection intropatterns: [= pats] - Use of this specific pattern also to apply discriminate on the fly Note: The automatic injection of dependent tuples over a same first component (introduced in r10180) still not integrated to the main parts of injection and its variant (indeed, it applies only for a root dependent tuple in sigT). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16621 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reorganizing intropatterns: * and ** are not naming intropatterns.Gravatar herbelin2013-07-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16620 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 17:26:33 +0000