| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-09-18 | Merge PR #8485: Missing space in cic.rst | Théo Zimmermann | |
| 2018-09-18 | Zify: replace local definitions by equations | Vincent Laporte | |
| 2018-09-18 | Removing Dischargedhypsmap which is unused internally. | Maxime Dénès | |
| The Dischargedhypsmap table collected the segment of section variables that constants defined in a section were originally depending on. It was useful to reconstruct the structure of sections as originally given in a source file. In particular this was used in Sacerdoti Coen's plugin for exportation of Coq files to xml. There is no information that this plugin, moved out of Coq in September 2014, was finally maintained, even as an external plugin. So it seems that the Dischargedhypsmap table is virtually not used anymore in the wild. Please contact the developers if ever the need for such a table happens to be necessary for your work. | |||
| 2018-09-17 | Add missing index entries. | Théo Zimmermann | |
| In particular, this backports e26b67436d12da63a11f0727c5b5895dfd03d249. | |||
| 2018-09-17 | Ensure_prev_proof returns a proof that has underlying differences from | Jim Fehrle | |
| the specified version (i.e., skip over versions with proofview-only differences). | |||
| 2018-09-17 | Merge PR #6906: [VM] Optimize structured values | Pierre-Marie Pédrot | |
| 2018-09-17 | Merge PR #8053: [dune] Add apidoc target using `odoc` | Gaëtan Gilbert | |
| 2018-09-17 | OCaml now exports the min and max non-constant tags, let's use it | Maxime Dénès | |
| 2018-09-17 | Add assertion on tags in eq_structured_constants | Maxime Dénès | |
| 2018-09-17 | [VM] Allocate a bit less in digits_from_uint | Maxime Dénès | |
| 2018-09-17 | [VM] Inject structured constants in values without reallocating them. | Maxime Dénès | |
| 2018-09-17 | [VM] Move structured_constant to Vmvalues | Maxime Dénès | |
| 2018-09-16 | Mising prime in the subtyping rules | Joachim Breitner | |
| 2018-09-16 | Missing space in cic.rst | Joachim Breitner | |
| 2018-09-15 | Overlay for cross-crypto. | Hugo Herbelin | |
| 2018-09-14 | Fixing yet a source of dependency on alphabetic order in unification. | Hugo Herbelin | |
| This refines even further c24bcae8 (PR #924) and 6304c843: - c24bcae8 fixed the order in the heuristic - 6304c843 improved the order by preferring projections There remained a dependency in the alphabetic order in selecting unification candidates. The current commit fixes it. We radically change the representation of the substitution to invert by using a map indexed on the rank in the signature rather than on the name of the variable. More could be done to use numbers further, e.g. for representing aliases. Note that this has consequences on the test-suite (in output/Notations.v) as some problems now infer a dependent return clause. | |||
| 2018-09-14 | Merge PR #7894: Remove quote plugin | Théo Zimmermann | |
| 2018-09-14 | Merge PR #8326: Mention PRINT_LOGS=1 when failing test suite | Enrico Tassi | |
| 2018-09-14 | Register: simpler syntax | Vincent Laporte | |
| 2018-09-14 | Retroknowledge: use GlobRef.t instead of Constr.t as entry | Vincent Laporte | |
| 2018-09-14 | Retroknowledge: simpler parsing rules | Vincent Laporte | |
| 2018-09-14 | Retroknowledge: remove the (unused) by clause | Vincent Laporte | |
| 2018-09-14 | Retroknowledge.KInt31: remove the (unused) group parameter | Vincent Laporte | |
| 2018-09-13 | Merge PR #8434: Canonical representation of kernel substitutions | Maxime Dénès | |
| 2018-09-13 | Merge PR #8436: Move maps & sets indexed by GlobRef.t into the kernel | Maxime Dénès | |
| 2018-09-13 | Merge PR #8303: Better controls for template polymorphism | Maxime Dénès | |
| 2018-09-13 | Add entry for universe polymorphism critical bug | Gaëtan Gilbert | |
| 2018-09-13 | Add test for inconsistency from polymorphism capturing global univs | Gaëtan Gilbert | |
| 2018-09-13 | Do not catch already declared universes in Environ.add_universes | Gaëtan Gilbert | |
| Include is still causing repeat declarations in add_universes_set | |||
| 2018-09-13 | Avoid repeat univ declaration in cumulative subtyping check | Gaëtan Gilbert | |
| 2018-09-13 | Avoid repeat universe declarations for constants with split univs | Gaëtan Gilbert | |
| 2018-09-13 | Do not redeclare universes for monomorphic operational typeclasses | Gaëtan Gilbert | |
| eg in [Class Foo (A:Type) := foo : A.] the universe should be declared when declaring the constant [Foo] and not [foo]. | |||
| 2018-09-13 | Add doc for template polymorphism option and attributes. | Gaëtan Gilbert | |
| 2018-09-13 | Add option to control automatic template polymorphism. | Gaëtan Gilbert | |
| 2018-09-13 | Add explicit atribute for template polymorphism. | Gaëtan Gilbert | |
| 2018-09-13 | Kernel: fully obey mind_entry_template | Gaëtan Gilbert | |
| 2018-09-13 | Elaboration: do not ask for small records to be template | Gaëtan Gilbert | |
| Imitating the kernel in anticipation for the kernel being more obedient | |||
| 2018-09-13 | Elaboration: do not ask poly inductives to be template | Gaëtan Gilbert | |
| 2018-09-13 | Elaboration: do not ask small inductives to be template | Gaëtan Gilbert | |
| This doesn't change behaviour currently as the kernel also makes this decision, but in the future it won't. | |||
| 2018-09-13 | Small simplification of elaboration side of template poly inductives | Gaëtan Gilbert | |
| 2018-09-13 | Mention PRINT_LOGS=1 when failing test suite | Gaëtan Gilbert | |
| It seems people don't always look at the test suite readme. | |||
| 2018-09-13 | Move test suite report script to standalone script file | Gaëtan Gilbert | |
| This allows for nicer formatting without having to deal with Make's semantic whitespace. | |||
| 2018-09-13 | Merge PR #8467: Manual: fix documentation of the “fresh” tactic | Théo Zimmermann | |
| 2018-09-13 | Merge PR #8470: Fix mli-doc following #7109. | Maxime Dénès | |
| 2018-09-12 | Fix mli-doc following #7109. | Théo Zimmermann | |
| 2018-09-12 | Move maps & sets indexed by GlobRef.t into the kernel | Vincent Laporte | |
| 2018-09-12 | Merge PR #8097: Use more efficient accu check for cofix unfolding in native ↵ | Maxime Dénès | |
| compilation. | |||
| 2018-09-12 | Merge PR #7109: Term combinators respecting the canonical structure of ↵ | Maxime Dénès | |
| branches and return predicate | |||
| 2018-09-12 | Remove quote plugin | Maxime Dénès | |
| As far as I know, this plugin is untested and barely maintained. I don't think it has real use cases any more, so let's move it out from the repo and see if somebody wants to take over and maintain it. We also remove the documentation, which was telling our users to look at ring to see an example of reification done using quote, when in fact it wasn't using it anymore. | |||
| 2018-09-12 | Manual: fix documentation of the “fresh” tactic | Vincent Laporte | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |