| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-05-23 | Fixing typos - Part 3 | JPR | |
| 2019-05-21 | Merge PR #10144: Fix #9919: conversion functions are non-linear | Hugo Herbelin | |
| Ack-by: herbelin Reviewed-by: maximedenes Ack-by: ppedrot | |||
| 2019-05-14 | Remove the sidecond_first flag of apply-related tactics. | Pierre-Marie Pédrot | |
| This was dead code. | |||
| 2019-05-14 | Remove the elimrename field from Tactics.eliminator. | Pierre-Marie Pédrot | |
| This is actually dead code, we never observe it. | |||
| 2019-05-14 | Code factorization in elim tactics. | Pierre-Marie Pédrot | |
| This is just moving code around, so it should not change the semantics. | |||
| 2019-05-11 | Actually use the conversion locality flag. | Pierre-Marie Pédrot | |
| Fixes #9919. | |||
| 2019-05-11 | Introducing a local flag to hypothesis conversion function. | Pierre-Marie Pédrot | |
| If the reduction function is known not to depend on the named context, then we can perform it in parallel on the various variables. | |||
| 2019-05-11 | Abstract the Tactic.e_change_hyps function over the reduction function. | Pierre-Marie Pédrot | |
| 2019-05-10 | Take advantage of the ordering / conversion check split. | Pierre-Marie Pédrot | |
| 2019-05-10 | Split the hypothesis conversion check in a conversion + ordering check. | Pierre-Marie Pédrot | |
| 2019-05-10 | Make the check flag of conversion functions mandatory. | Pierre-Marie Pédrot | |
| The current situation is a mess, some functions set it by default, but other no. Making it mandatory ensures that the expected value is the correct one. | |||
| 2019-05-10 | Logic.convert_hyp now takes an environment as an argument. | Pierre-Marie Pédrot | |
| This prevents having to call global functions, for no good reason. We also seize the opportunity to name the check argument. | |||
| 2019-05-03 | Tactics: fixing "change_no_check in". | Hugo Herbelin | |
| (Merge of the initial version with #9983 was broken) | |||
| 2019-05-03 | Fix #9994: `revert dependent` is extremely slow. | Pierre-Marie Pédrot | |
| We add a fast path when generalizing over variables. | |||
| 2019-04-29 | Exposing a change_no_check tactic. | Hugo Herbelin | |
| 2019-04-24 | Allocate only one evar when applying a group of conversion tactics. | Pierre-Marie Pédrot | |
| 2019-04-24 | Code factorization in conversion tactics. | Pierre-Marie Pédrot | |
| 2019-04-23 | Deprecate the *_no_check variants of conversion tactics. | Pierre-Marie Pédrot | |
| 2019-04-10 | Remove calls to global env in Inductiveops | Maxime Dénès | |
| 2019-04-10 | Remove calls to global env from indrec | Maxime Dénès | |
| 2019-03-27 | [geninterp] Track polymorphic status in tactic interpretation. | Emilio Jesus Gallego Arias | |
| 2019-03-14 | Add relevance marks on binders. | Gaëtan Gilbert | |
| Kernel should be mostly correct, higher levels do random stuff at times. | |||
| 2019-03-14 | Add a non-cumulative impredicative universe SProp. | Gaëtan Gilbert | |
| Note currently it's impossible to define inductives in SProp because indtypes.ml and the pretyper aren't fully plugged. | |||
| 2019-02-08 | Change interfaces of evarconv as suggested by Enrico. | Matthieu Sozeau | |
| Now the main functions are unify (solves the problems entirely) and unify_delay and unify_leq (which might leave some unsolved constraints). Deprecated the_conv_x and the_conv_x_leq (which were misnommers as they do unification not conversion). | |||
| 2019-02-08 | Merge PR #9410: Make `Program` a regular attribute | Matthieu Sozeau | |
| Ack-by: SkySkimmer Reviewed-by: aspiwack Reviewed-by: ejgallego Reviewed-by: gares Reviewed-by: mattam82 Ack-by: maximedenes | |||
| 2019-02-06 | Avoid eqn when generating name in induction_gen. | Jasper Hugunin | |
| Fixes #9494. Was failing with "Cannot create self-referring hypothesis" when the generated name equaled the eqn. | |||
| 2019-02-05 | Make Program a regular attribute | Maxime Dénès | |
| We remove all calls to `Flags.is_program_mode` except one (to compute the default value of the attribute). Everything else is passed explicitely, and we remove the special logic in the interpretation loop to set/unset the flag. This is especially important since the value of the flag has an impact on proof modes, so on the separation of parsing and execution phases. | |||
| 2019-01-23 | Move and rewrite documentation for intro patterns that was under | Jim Fehrle | |
| the intros tactic to its own subsection. Add grammar and examples. | |||
| 2018-12-19 | Merge PR #9139: [engine] Allow debug printers to access the environment. | Pierre-Marie Pédrot | |
| 2018-12-18 | Merge PR #9160: Avoid user-given names in automatic introduction of binders | Pierre-Marie Pédrot | |
| 2018-12-17 | Merge PR #9153: [api] Move reduction modules to `tactics` | Pierre-Marie Pédrot | |
| 2018-12-15 | Avoid explicit names in binders for automatic intros | Jasper Hugunin | |
| 2018-12-13 | [engine] Allow debug printers to access the environment. | Emilio Jesus Gallego Arias | |
| This should improve correctness and will be needed for the PRs that remove global access to the proof state. | |||
| 2018-12-11 | [api] Move reduction modules to `tactics` | Emilio Jesus Gallego Arias | |
| These modules do actually belong there. We have to slightly reorganize printers, removing a couple of duplicated ones in the way. | |||
| 2018-12-09 | [doc] Enable Warning 50 [incorrect doc comment] and fix comments. | Emilio Jesus Gallego Arias | |
| This is a pre-requisite to use automated formatting tools such as `ocamlformat`, also, there were quite a few places where the comments had basically no effect, thus it was confusing for the developer. p.s: Reading some comments was a lot of fun :) | |||
| 2018-11-23 | s/let _ =/let () =/ in some places (mostly goptions related) | Gaëtan Gilbert | |
| 2018-11-21 | [legacy proof engine] Remove some cruft. | Emilio Jesus Gallego Arias | |
| We remove the `Proof_types` file which was a trivial stub, we also cleanup a few layers of aliases. This is not a lot but every little step helps. | |||
| 2018-11-19 | Rename TranspState into TransparentState. | Pierre-Marie Pédrot | |
| 2018-11-19 | Move transparent_state to its own module. | Pierre-Marie Pédrot | |
| 2018-11-16 | Remove the implicit tactic feature following #7229. | Pierre-Marie Pédrot | |
| 2018-11-08 | Standardize handling of Automatic Introduction. | Jasper Hugunin | |
| This fixes #8791. We explicitly specify for intro the names of binders which are given by the user. This still can suffer from spurious collisions, see #8819. | |||
| 2018-11-05 | Merge PR #8866: Check universe instances in Typing | Pierre-Marie Pédrot | |
| 2018-10-30 | Fix evar leak in induction tactic. | Gaëtan Gilbert | |
| Detected when making Typing check universe instances. | |||
| 2018-10-30 | Move abstract out of tactics.ml | Gaëtan Gilbert | |
| 2018-10-26 | Cleanup evar_extra: remove evar_info's store and add maps to evar_map | Matthieu Sozeau | |
| 2018-10-14 | Passing env functionally in move_hyp and insert_decl_in_named_context. | Hugo Herbelin | |
| 2018-10-10 | [coqlib] Rebindable Coqlib namespace. | Emilio Jesus Gallego Arias | |
| We refactor the `Coqlib` API to locate objects over a namespace `module.object.property`. This introduces the vernacular command `Register g as n` to expose the Coq constant `g` under the name `n` (through the `register_ref` function). The constant can then be dynamically located using the `lib_ref` function. Co-authored-by: Emilio Jesús Gallego Arias <e+git@x80.org> Co-authored-by: Maxime Dénès <mail@maximedenes.fr> Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr> | |||
| 2018-10-08 | Remove dead code in universe handling in the abstract tactical. | Pierre-Marie Pédrot | |
| Since 213b323 the kernel was expecting to receive an empty set of internal universe constraints in polymorphic definitions. We lift this invariant to the code that actually generates side effects. | |||
| 2018-09-27 | Fixes #8553 (regression of tactic "change" under binders). | Hugo Herbelin | |
| 2018-09-24 | [engine] Remove and deprecate `nf_enter` et al. | Emilio Jesus Gallego Arias | |
| After the introduction of `EConstr`, "normalization" has become unnecessary, we thus deprecate the `nf_*` family of functions. Test-suite and CI pass after the fix for #8513. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |