| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-08-24 | Merge PR #12565: Dnets now consider axioms as being opaque for pattern ↵ | coqbot | |
| recognition. Reviewed-by: mattam82 | |||
| 2020-08-24 | Merge PR #12816: Fixes #12787: anomaly of tactic injection in the presence ↵ | Pierre-Marie Pédrot | |
| of artificial dependencies disappearing by reduction Reviewed-by: ppedrot | |||
| 2020-08-20 | Use properly fresh names for Scheme Equality | Jasper Hugunin | |
| 2020-08-20 | Quick fix to #12787 (injection anomaly due to inconsistent comp. of free vars). | Hugo Herbelin | |
| We fix it by reducing K-redexes the same in the both places (make_tuple and minimal_free_rels) which compute the dependencies of a dependent equality. | |||
| 2020-08-20 | Do not store the transparent state in delayed dnets. | Pierre-Marie Pédrot | |
| We know statically that it is going to be the one provided at the time of lookup, so we simply fetch it from there. | |||
| 2020-08-20 | Dnets now consider axioms as being opaque for pattern recognition. | Pierre-Marie Pédrot | |
| 2020-08-19 | Replace Hints.head_constr_bound with Hints.head_bound. | Pierre-Marie Pédrot | |
| The two implementations are essentially the same except for potential interleaving of let-bindings and pattern-matchings. The only place the removed function was called probably does not rely on this difference of behaviour. | |||
| 2020-08-19 | Simplify the computation of the head global for hint patterns. | Pierre-Marie Pédrot | |
| Instead of having to go through the pattern translation, we compute the pattern directly from the term. | |||
| 2020-08-19 | Ensure statically that Hint Extern comes with a pattern. | Pierre-Marie Pédrot | |
| 2020-08-19 | Merge PR #12822: Do not precompute hint dnets eagerly | Matthieu Sozeau | |
| Reviewed-by: mattam82 | |||
| 2020-08-19 | Merge PR #12725: Store evar identity instances in evarinfo / named_context_val | Enrico Tassi | |
| Ack-by: SkySkimmer Reviewed-by: gares | |||
| 2020-08-17 | Merge PR #12841: Recommend replace as a replacement to cutrewrite. | coqbot | |
| Reviewed-by: jfehrle Reviewed-by: ppedrot | |||
| 2020-08-17 | Recommend replace as a replacement to cutrewrite. | Théo Zimmermann | |
| As suggested by Laurent Thery to Chris Dams on Coq-Club. (And fix the documented syntax in the manual.) | |||
| 2020-08-17 | Merge PR #12751: Fixes reduction effect printing in the presence of non ↵ | Pierre-Marie Pédrot | |
| purely applicative stacks Ack-by: SkySkimmer Reviewed-by: ppedrot | |||
| 2020-08-14 | Do not precompute hint dnets eagerly. | Pierre-Marie Pédrot | |
| Due to the way transparency is handled in hint databases, every time it is changed, all dnets are recomputed from scratch. This is very expensive, and a bench showed that it was sometimes contributing significantly to the whole compilation time of hint-heavy libraries. This patch makes this computation lazy, so that the dnet is computed only the first time a hint lookup is performed. The implementation is functionally equivalent to wrapping the sentry_bnet field in a Lazy.t, but because dnets are stored in the summary and thus marshalled, I had to manually perform a defunctionalization. A (maybe cleaner?) alternative would be to track the set of constants a hint depend on, in order to only refresh those touched by the change of transparency. Yet, this would be a much more invasive change. | |||
| 2020-08-13 | Merge PR #12720: Factor code related to class hint clenv | Hugo Herbelin | |
| Reviewed-by: SkySkimmer Reviewed-by: herbelin | |||
| 2020-08-13 | Merge PR #12718: Do not rely on higher-order interfaces for patterns in dnets. | Hugo Herbelin | |
| Reviewed-by: herbelin | |||
| 2020-08-12 | Cosmetic changes as suggested by SkySkimmer. | Pierre-Marie Pédrot | |
| 2020-08-12 | Further code simplification in typeclass resolution tactic. | Pierre-Marie Pédrot | |
| 2020-08-12 | Split the uses of connect_hint_clenv into two different functions. | Pierre-Marie Pédrot | |
| The first one is encapsulating the clenv part, and is now purely internal, while the other one provides an abstract interfact to get fresh term instances from a hint. | |||
| 2020-08-12 | Tentatively more efficient implementation of e_give_exact for typeclasses. | Pierre-Marie Pédrot | |
| The old code was refreshing the whole evarmap when only the constraints introduced by the term would matter. Since exact hints never introduces metas for missing binders, there is nothing to extract from the clenv, so we can just generate a fresh universe substitution. | |||
| 2020-08-12 | Export a dedicated function that applies immediately a hint. | Pierre-Marie Pédrot | |
| 2020-08-12 | Code simplification around hint manipulation in Class_tactics. | Pierre-Marie Pédrot | |
| We inline the clenv universe refreshing, since it was the only place in the code that used it. Furthermore it was performing useless substitutions in the clenv. | |||
| 2020-08-12 | Make the Hint.hint type private. | Pierre-Marie Pédrot | |
| 2020-08-12 | Move connect_hint_clenv from Auto to Hints. | Pierre-Marie Pédrot | |
| 2020-08-12 | Do not do a round trip with auto hint representation in autoapply. | Pierre-Marie Pédrot | |
| 2020-08-12 | Do not tamper with hints in Class_tactics.with_prods. | Pierre-Marie Pédrot | |
| 2020-08-12 | Perfom an goal enter in the relevant class tactics instead of outside. | Pierre-Marie Pédrot | |
| 2020-08-12 | Inline Class_tactics.clenv_of_prods. | Pierre-Marie Pédrot | |
| It was unnecessarily obfuscated. | |||
| 2020-08-10 | Merge PR #12749: [ssr] turn "nothing to inject" into a real warning (fix #12746) | Cyril Cohen | |
| Reviewed-by: CohenCyril Reviewed-by: SkySkimmer Ack-by: Zimmi48 Ack-by: maximedenes Ack-by: ppedrot | |||
| 2020-08-10 | [ssr] turn "nothing to inject" into a real warning (fix #12746) | Enrico Tassi | |
| 2020-08-06 | Actually use the default instance stored inside named_context_val. | Pierre-Marie Pédrot | |
| 2020-08-06 | Remove several calls to Evarutil.new_pure_evar. | Pierre-Marie Pédrot | |
| 2020-07-27 | Do not rely on higher-order interfaces for patterns in dnets. | Pierre-Marie Pédrot | |
| The old API was taking a function to decompose constr patterns into dnet patterns, but it was applying it in an eager way. So there is not point in exposing such a complex interface. Instead, we make explicit the dnet pattern type, export a function that turns a constr pattern into a dnet pattern, and make the add and remove dnet functions take a dnet pattern instead. This only affects pattern-consuming functions. The lookup function, which operates on kernel terms instead of constr patterns, is still relying on HO primitives. | |||
| 2020-07-24 | Fixes reduction effect printing in the presence of non purely applicative ↵ | Hugo Herbelin | |
| stacks. | |||
| 2020-07-22 | Clarify Global.env usage in ppvernac | Gaëtan Gilbert | |
| 2020-07-09 | [exn] Remove some uses of print | Emilio Jesus Gallego Arias | |
| Exceptions should not printed except for the top-level. There is the weird anomaly-absorbing code in `Reductionops`, I wonder how frequent that case is, but as the exception is absorbed printing there could have a real impact. | |||
| 2020-07-08 | Remove Evarutil.new_evar_instance from the API. | Pierre-Marie Pédrot | |
| 2020-07-08 | Remove Evarutil.new_evar_from_context from the API. | Pierre-Marie Pédrot | |
| 2020-07-06 | Merge PR #11604: Primitive persistent arrays | Pierre-Marie Pédrot | |
| Ack-by: JasonGross Ack-by: SkySkimmer Ack-by: ejgallego Ack-by: gares Reviewed-by: ppedrot Ack-by: proux01 Ack-by: silene | |||
| 2020-07-06 | Primitive persistent arrays | Maxime Dénès | |
| Persistent arrays expose a functional interface but are implemented using an imperative data structure. The OCaml implementation is based on Jean-Christophe Filliâtre's. Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr> Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | |||
| 2020-07-06 | Merge PR #12622: Use goal cycling instead of manual evar generation order in ↵ | Gaëtan Gilbert | |
| internal_cut_rev Reviewed-by: SkySkimmer | |||
| 2020-07-03 | Merge PR #10390: UIP in SProp | Maxime Dénès | |
| Reviewed-by: Zimmi48 Ack-by: ejgallego Reviewed-by: maximedenes | |||
| 2020-07-02 | Merge PR #12572: Correctly classify variables as being unfoldable in dnet ↵ | Gaëtan Gilbert | |
| patterns. Reviewed-by: SkySkimmer Reviewed-by: maximedenes | |||
| 2020-07-01 | Use goal cycling instead of manual evar generation order in internal_cut_rev. | Pierre-Marie Pédrot | |
| This reduces the combinatorial complexity of the function, and the code size as well. | |||
| 2020-07-01 | UIP in SProp | Gaëtan Gilbert | |
| 2020-06-30 | Merge PR #12599: Remove the Refiner module | Emilio Jesus Gallego Arias | |
| Reviewed-by: ejgallego | |||
| 2020-06-29 | Merge PR #12541: Fix #12228 negative integers not accepted in ltac integer_list | Pierre-Marie Pédrot | |
| Reviewed-by: ppedrot | |||
| 2020-06-29 | Move the FailError exception from Refiner to Tacticals. | Pierre-Marie Pédrot | |
| 2020-06-29 | Moving the remaining Refiner functions to Tacmach. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |