| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-11-13 | [api] Insert miscellaneous API deprecation back to core. | Emilio Jesus Gallego Arias | |
| 2017-11-13 | [api] Another large deprecation, `Nameops` | Emilio Jesus Gallego Arias | |
| 2017-11-06 | [api] Move structures deprecated in the API to the core. | Emilio Jesus Gallego Arias | |
| We do up to `Term` which is the main bulk of the changes. | |||
| 2017-11-06 | [api] Deprecate all legacy uses of Names in core. | Emilio Jesus Gallego Arias | |
| This will allow to merge back `Names` with `API.Names` | |||
| 2017-11-06 | Merge PR #6064: [api] Deprecate all legacy uses of Name.Id in core. | Maxime Dénès | |
| 2017-11-05 | Cosmetic changes in evar_map printer. | Hugo Herbelin | |
| 2017-11-05 | Preventively protect locally against failures of evar_map printer. | Hugo Herbelin | |
| It is not clear that this is really needed, but in case it happens, one will at least have a partial result available rather than an unexploitable global failure of the parser. | |||
| 2017-11-05 | Fixing a cause of failure of evar_map printer in debugger. | Hugo Herbelin | |
| Indeed, the debugger debugs coqtop but it is itself just an ocaml runtime extended with the coq printers. It does not know the environment, so, looking in the Global.env() for the printers can only fail. | |||
| 2017-11-04 | [api] Deprecate all legacy uses of Name.Id in core. | Emilio Jesus Gallego Arias | |
| This is a first step towards some of the solutions proposed in #6008. | |||
| 2017-11-03 | Merge PR #6051: Fix FIXME: use OCaml 4.02 generative functors when available. | Maxime Dénès | |
| 2017-11-03 | Merge PR #6047: A generic printer for ltac values | Maxime Dénès | |
| 2017-11-02 | Exporting ValTMap for use in Genintern. | Hugo Herbelin | |
| 2017-11-01 | Fix FIXME: use OCaml 4.02 generative functors when available. | Gaëtan Gilbert | |
| 4.02.3 has been the minimal OCaml version for a while now. | |||
| 2017-10-28 | Fixing #5401 (printing of patterns with bound anonymous variables). | Hugo Herbelin | |
| This fixes also #5731, #6035, #5364. | |||
| 2017-10-09 | Merge PR #1109: Handle some misc todos | Maxime Dénès | |
| 2017-10-06 | Merge PR #1119: Fixing bug BZ#5769 (generating a name "_" out of a type ↵ | Maxime Dénès | |
| "_something") | |||
| 2017-10-05 | Merge PR #1102: On the detection of evars which "advanced" (and a fix to ↵ | Maxime Dénès | |
| BZ#5757) | |||
| 2017-10-05 | Merge PR #1101: Fixing an old proof engine bug in collecting evars with ↵ | Maxime Dénès | |
| cleared context. | |||
| 2017-10-05 | Fixing BZ#5769 (variable of type "_something" was named after invalid "_"). | Hugo Herbelin | |
| 2017-09-29 | Remove TODO comment (Evar.t is opaque) | Gaëtan Gilbert | |
| 2017-09-28 | Efficient computation of the names contained in an environment. | Pierre-Marie Pédrot | |
| 2017-09-28 | Efficient fresh name generation relying on sets. | Pierre-Marie Pédrot | |
| The old algorithm was relying on list membership, which is O(n). This was nefarious for terms with many binders. We use instead sets in O(log n). | |||
| 2017-09-27 | Moving setting of "cleared" evar flag directly in Evd.restrict. | Hugo Herbelin | |
| In particular, this fixes #5757 which used restrict_evar to refine the information on the source of an evar, and which should have set the "cleared" flag. Also renaming flag "restricted" since it is not only about "clear". I guess this is what we want in general, but I did not survey all uses of restrict_evar so, maybe, this should be refined further. | |||
| 2017-09-27 | Fixing an old bug in collecting evars with cleared context. | Hugo Herbelin | |
| The function Proofview.undefined was collecting twice the evars that had advanced. Consequently, the functions Proofview.unshelve and Proofview.with_shelf were possibly doing the same. | |||
| 2017-09-27 | Fixing an old bug in collecting evars with cleared context. | Hugo Herbelin | |
| The function Proofview.undefined was collecting twice the evars that had advanced. Consequently, the functions Proofview.unshelve and Proofview.with_shelf were possibly doing the same. | |||
| 2017-09-26 | Merge PR #688: Binding universe constraints in Definition/Inductive/etc... | Maxime Dénès | |
| 2017-09-19 | Merge PR #1036: Unify EConstr.t equality | Maxime Dénès | |
| 2017-09-19 | Document UState.universe_context. | Gaëtan Gilbert | |
| 2017-09-19 | Don't lose names in UState.universe_context. | Gaëtan Gilbert | |
| We dont care about the order of the binder map ([map] in the code) so no need to do tricky things with it. | |||
| 2017-09-19 | proof_global: cleanup and comment close_proof | Matthieu Sozeau | |
| evd: Move constrain_variables to an operation on UState Necessary to check universe declarations correctly for deferred proofs in particular. | |||
| 2017-09-19 | Allow declaring universe constraints at definition level. | Matthieu Sozeau | |
| Introduce a "+" modifier for universe and constraint declarations to indicate that these can be extended in the final definition/proof. By default [Definition f] is equivalent to [Definition f@{+|+}], i.e universes can be introduced and constraints as well. For [f@{}] or [f@{i j}], the constraints can be extended, no universe introduced, to maintain compatibility with existing developments. Use [f@{i j | }] to indicate that no constraint (nor universe) can be introduced. These kind of definitions could benefit from asynchronous processing. Declarations of universe binders and constraints also works for monomorphic definitions. | |||
| 2017-09-12 | Port is_Set and is_Type to EConstr, as was is_Prop already. | Guillaume Melquiond | |
| 2017-09-08 | Normalizing universes before performing term comparison. | Pierre-Marie Pédrot | |
| This code was probably slightly wrong w.r.t. to a semantics defined as equivalent to first full-blown normalization followed by kernel term equality. Or at least, it was adding redundant constraints. | |||
| 2017-09-08 | Using EConstr equality check in unification. | Pierre-Marie Pédrot | |
| The code from Universes what essentially a duplicate of the one from EConstr, but they were copied for historical reasons. Now, this is not useful anymore, so that we remove the implementation from Universes and rely on the one from EConstr. | |||
| 2017-08-29 | Merge PR #830: Moving assert (the "Cut" rule) to new proof engine | Maxime Dénès | |
| 2017-08-01 | Merge PR #913: Less allocations in Detyping | Maxime Dénès | |
| 2017-07-31 | Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t instead | Maxime Dénès | |
| 2017-07-27 | deprecate Pp.std_ppcmds type alias | Matej Košík | |
| 2017-07-26 | Removing template polymorphism for definitions. | Pierre-Marie Pédrot | |
| The use of template polymorphism in constants was quite limited, as it only applied to definitions that were exactly inductive types without any parameter whatsoever. Furthermore, it seems that following the introduction of polymorphic definitions, the code path enforced regular polymorphism as soon as the type of a definition was given, which was in practice almost always. Removing this feature had no observable effect neither on the test-suite, nor on any development that we monitor on Travis. I believe it is safe to assume it was nowadays useless. | |||
| 2017-07-21 | No useless reallocation in Termops.collapse_appl. | Pierre-Marie Pédrot | |
| This function is suspicious, and reallocates a lot when it should be the identity. This matters for detyping, where it is about the only place where it is used. | |||
| 2017-07-19 | [proofs] Remove circular dependency from Proofview to Goal. | Emilio Jesus Gallego Arias | |
| 2017-07-17 | Merge PR #781: Remove dead code [Universes.simplify_universe_context] | Maxime Dénès | |
| 2017-07-13 | Safer API for constr_of_global, and getting rid of unsafe_constr_of_global. | Pierre-Marie Pédrot | |
| 2017-07-13 | Merge PR #870: Prepare De Bruijn universe abstractions, Episode I: Kernel | Maxime Dénès | |
| 2017-07-11 | Less footguns in universe handling: remove subst_instance_context. | Pierre-Marie Pédrot | |
| This function was lurking around, waiting to bite anybody willing to use it. We use instead a better API, correct and much less error-prone. | |||
| 2017-07-11 | Getting rid of simple calls to AUContext.instance. | Pierre-Marie Pédrot | |
| This function breaks the abstraction barrier of abstract universe contexts, as it provides a way to observe the bound names of such a context. We remove all the uses that can be easily get rid of with the current API. | |||
| 2017-07-07 | Merge PR #816: In enter_one, not having exactly one goal is a fatal error of ↵ | Maxime Dénès | |
| the monad. | |||
| 2017-07-04 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2017-07-04 | Bump year in headers. | Pierre-Marie Pédrot | |
| 2017-06-25 | Adding intermediate entry point to create an evar in empty rel_context. | Hugo Herbelin | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |