| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-07-17 | change into QuestionMark default | Siddharth Bhat | |
| 2018-07-17 | Change QuestionMark for better record field missing error message. | Siddharth Bhat | |
| While we were adding a new field into `QuestionMark`, we decided to go ahead and refactor the constructor to hold an actual record. This record now holds the name, obligations, and whether the evar represents a missing record field. This is used to provide better error messages on missing record fields. | |||
| 2018-07-03 | Evarutil.(e_)new_Type: remove unused env argument | Gaëtan Gilbert | |
| 2018-07-03 | Remove unused function Evd.whd_sort_variable | Gaëtan Gilbert | |
| 2018-07-03 | Remove unused output of Universes.normalize_univ_variables | Gaëtan Gilbert | |
| 2018-07-03 | Remove unused env argument to fresh_sort_in_family | Gaëtan Gilbert | |
| (Universes and Evd) | |||
| 2018-06-27 | Swapping Context and Constr: defining declarations on constr in Constr. | Hugo Herbelin | |
| This shall eventually allow to use contexts of declarations in the definition of the "Case" constructor. Basically, this means that Constr now includes Context and that the "t" types of Context which were specialized on constr are not defined in Constr (unfortunately using a heavy boilerplate). | |||
| 2018-06-27 | Merge PR #7863: Remove Sorts.contents | Pierre-Marie Pédrot | |
| 2018-06-26 | Merge PR #7826: evd: restrict_evar with candidates, can raise NoCandidatesLeft | Hugo Herbelin | |
| 2018-06-26 | Merge PR #7906: universes_of_constr don't include universes of monomorphic ↵ | Pierre-Marie Pédrot | |
| constants | |||
| 2018-06-26 | Remove Sorts.contents | Gaëtan Gilbert | |
| 2018-06-26 | universes_of_constr don't include universes of monomorphic constants | Gaëtan Gilbert | |
| Apparently it was not useful. I don't remember what I was thinking when I added it. | |||
| 2018-06-23 | Merge PR #7827: [engine] safe [add_unification_pb] interface | Pierre-Marie Pédrot | |
| 2018-06-19 | Merge PR #7797: Remove reference name type. | Enrico Tassi | |
| 2018-06-18 | Fix #7421: constr_eq ignores universe constraints. | Gaëtan Gilbert | |
| The test isn't quite the one in #7421 because that use of algebraic universes is wrong. | |||
| 2018-06-18 | Remove reference name type. | Maxime Dénès | |
| reference was defined as Ident or Qualid, but the qualid type already permits empty paths. So we had effectively two representations for unqualified names, that were not seen as equal by eq_reference. We remove the reference type and replace its uses by qualid. | |||
| 2018-06-15 | evd: restrict_evar with candidates, can raise NoCandidatesLeft | Matthieu Sozeau | |
| When restricting an evar with candidates, raise an exception if this restriction would leave the evar without candidates, i.e. unsolvable. - evarutil: mark restricted evars as "cleared" They would otherwise escape being catched by the [advance] function of clenv, and result in dangling evars not being registered to the shelf. - engine: restrict_evar marks it cleared, update the future goals We make the new evar a future goal and remove the old one. If we did nothing, [unshelve tac] would work correctly as it uses [Proofview.advance] to find the shelved goals, going through the cleared evar. But [Unshelve] would fail as it expects only undefined evars on the shelf and throws away the defined ones. | |||
| 2018-06-15 | evd/evarutil: safe [add_unification_pb] interface, taking EConstr's | Matthieu Sozeau | |
| Avoid adding the same unification problem twice, module evar instantiation. | |||
| 2018-06-12 | [api] Misctypes removal: several moves: | Emilio Jesus Gallego Arias | |
| - move_location to proofs/logic. - intro_pattern_naming to Namegen. | |||
| 2018-06-12 | [api] Misctypes removal: miscellaneous aliases. | Emilio Jesus Gallego Arias | |
| 2018-06-08 | Add a bit of doc to EConstr.decompose_lam* | Gaëtan Gilbert | |
| 2018-06-07 | Merge PR #7706: Fix wrong deprecation msg | Pierre-Marie Pédrot | |
| 2018-06-07 | Merge PR #6874: [econstr] Some minor tweaks | Pierre-Marie Pédrot | |
| 2018-06-05 | Update evarutil.mli | Matthieu Sozeau | |
| Actually all the new_ functions are in evarutil still | |||
| 2018-06-05 | Fix wrong deprecation msg | Matthieu Sozeau | |
| 2018-06-05 | Merge PR #7495: Fix restrict_universe_context | Matthieu Sozeau | |
| 2018-06-04 | [econstr] Remove some Unsafe.to_constr use. | Emilio Jesus Gallego Arias | |
| Most of it seems straightforward. | |||
| 2018-06-04 | [termops] Update type of function, anyways not used in the codebase. | Emilio Jesus Gallego Arias | |
| Note that `Assumptions` ships its own copy, but for `Constr.t`. | |||
| 2018-06-04 | Merge PR #7216: Replace uses of Termops.dependent by more specific functions. | Matthieu Sozeau | |
| 2018-05-31 | [api] Move `Constrexpr` to the `interp` module. | Emilio Jesus Gallego Arias | |
| Continuing the interface cleanup we place `Constrexpr` in the internalization module, which is the one that eliminates it. This slims down `pretyping` considerably, including removing the `Univdecls` module which existed only due to bad dependency ordering in the first place. Thanks to @ Skyskimmer we also remove a duplicate `univ_decl` definition among `Misctypes` and `UState`. This is mostly a proof of concept yet as it depends on quite a few patches of the tree. For sure some tweaks will be necessary, but it should be good for review now. IMO the tree is now in a state where we can could easy eliminate more than 10 modules without any impact, IMHO this is a net saving API-wise and would help people to understand the structure of the code better. | |||
| 2018-05-30 | [api] Remove deprecated objects in engine / interp / library | Emilio Jesus Gallego Arias | |
| 2018-05-30 | [api] Remove deprecated object from `Term` | Emilio Jesus Gallego Arias | |
| We remove most of what was deprecated in `Term`. Now, `intf` and `kernel` are almost deprecation-free, tho I am not very convinced about the whole `Term -> Constr` renaming but I'm afraid there is no way back. Inconsistencies with the constructor policy (see #6440) remain along the code-base and I'm afraid I don't see a plan to reconcile them. The `Sorts` deprecation is hard to finalize, opening `Sorts` is not a good idea as someone added a `List` module inside it. | |||
| 2018-05-30 | Fix restrict_universe_context | Gaëtan Gilbert | |
| 2018-05-28 | Merge PR #7521: Fix soundness bug with VM/native and cofixpoints | Pierre-Marie Pédrot | |
| 2018-05-28 | Unify pre_env and env | Maxime Dénès | |
| We now have only two notions of environments in the kernel: env and safe_env. | |||
| 2018-05-25 | Remove some occurrences of Evd.empty | Maxime Dénès | |
| We address the easy ones, but they should probably be all removed. | |||
| 2018-05-23 | Collecting Map.smart_* functions into a module Map.Smart. | Hugo Herbelin | |
| 2018-05-23 | Exporting Fun1 within Array so that Array.Fun1 and not only CArray.Fun1 works. | Hugo Herbelin | |
| 2018-05-23 | Collecting Array.smart_* functions into a module Array.Smart. | Hugo Herbelin | |
| 2018-05-17 | Split off Universes functions for minimization. | Gaëtan Gilbert | |
| This finishes the splitting of Universes. | |||
| 2018-05-17 | Make Universes.refresh_constraints internal to UState | Gaëtan Gilbert | |
| 2018-05-17 | Split off Universes functions about substitutions and constraints | Gaëtan Gilbert | |
| 2018-05-17 | Move solve_constraint_system near its only use site (comInductive) | Gaëtan Gilbert | |
| 2018-05-17 | Split off Universes functions dealing with generating new universes. | Gaëtan Gilbert | |
| 2018-05-17 | Split off Universes functions dealing with names. | Gaëtan Gilbert | |
| This API is a bit strange, I expect it will change at some point. | |||
| 2018-05-17 | Make set minimization option internal to Universes | Gaëtan Gilbert | |
| 2018-05-17 | Merge PR #7359: Reduce usage of evar_map references | Pierre-Marie Pédrot | |
| 2018-05-14 | Use evd_combX in Cases. | Gaëtan Gilbert | |
| 2018-05-11 | Convert clear_hyps_in_evi to state passing style. | Gaëtan Gilbert | |
| 2018-05-11 | Deprecate most evarutil evdref functions | Gaëtan Gilbert | |
| clear_hyps remain with no alternative | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |