aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-09-19Merge PR #7343: Add missing index entries.Maxime Dénès
2018-09-19Merge PR #8341: Reduce universe redeclarations (catching AlreadyDeclared)Matthieu Sozeau
2018-09-19Merge PR #8071: Propose a Code of Conduct for Coq.Matthieu Sozeau
2018-09-19Merge PR #7257: Fixing yet a source of dependency on alphabetic order in ↵Pierre-Marie Pédrot
unification.
2018-09-19Merge PR #8447: Cleaning in the retroknowledgePierre-Marie Pédrot
2018-09-19Merge PR #8463: Remove DischargedhypsmapsPierre-Marie Pédrot
2018-09-18Merge PR #8486: Mising prime in the subtyping rulesThéo Zimmermann
2018-09-18Merge PR #8485: Missing space in cic.rstThéo Zimmermann
2018-09-18Removing 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-17Add missing index entries.Théo Zimmermann
In particular, this backports e26b67436d12da63a11f0727c5b5895dfd03d249.
2018-09-17Merge PR #6906: [VM] Optimize structured valuesPierre-Marie Pédrot
2018-09-17Merge PR #8053: [dune] Add apidoc target using `odoc`Gaëtan Gilbert
2018-09-17OCaml now exports the min and max non-constant tags, let's use itMaxime Dénès
2018-09-17Add assertion on tags in eq_structured_constantsMaxime Dénès
2018-09-17[VM] Allocate a bit less in digits_from_uintMaxime 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 VmvaluesMaxime Dénès
2018-09-16Mising prime in the subtyping rulesJoachim Breitner
2018-09-16Missing space in cic.rstJoachim Breitner
2018-09-15Overlay for cross-crypto.Hugo Herbelin
2018-09-14Fixing 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-14Merge PR #7894: Remove quote pluginThéo Zimmermann
2018-09-14Merge PR #8326: Mention PRINT_LOGS=1 when failing test suiteEnrico Tassi
2018-09-14Register: simpler syntaxVincent Laporte
2018-09-14Retroknowledge: use GlobRef.t instead of Constr.t as entryVincent Laporte
2018-09-14Retroknowledge: simpler parsing rulesVincent Laporte
2018-09-14Retroknowledge: remove the (unused) by clauseVincent Laporte
2018-09-14Retroknowledge.KInt31: remove the (unused) group parameterVincent Laporte
2018-09-13Merge PR #8434: Canonical representation of kernel substitutionsMaxime Dénès
2018-09-13Merge PR #8436: Move maps & sets indexed by GlobRef.t into the kernelMaxime Dénès
2018-09-13Merge PR #8303: Better controls for template polymorphismMaxime Dénès
2018-09-13Add entry for universe polymorphism critical bugGaëtan Gilbert
2018-09-13Add test for inconsistency from polymorphism capturing global univsGaëtan Gilbert
2018-09-13Do not catch already declared universes in Environ.add_universesGaëtan Gilbert
Include is still causing repeat declarations in add_universes_set
2018-09-13Avoid repeat univ declaration in cumulative subtyping checkGaëtan Gilbert
2018-09-13Avoid repeat universe declarations for constants with split univsGaëtan Gilbert
2018-09-13Do not redeclare universes for monomorphic operational typeclassesGaë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-13Add doc for template polymorphism option and attributes.Gaëtan Gilbert
2018-09-13Add option to control automatic template polymorphism.Gaëtan Gilbert
2018-09-13Add explicit atribute for template polymorphism.Gaëtan Gilbert
2018-09-13Kernel: fully obey mind_entry_templateGaëtan Gilbert
2018-09-13Elaboration: do not ask for small records to be templateGaëtan Gilbert
Imitating the kernel in anticipation for the kernel being more obedient
2018-09-13Elaboration: do not ask poly inductives to be templateGaëtan Gilbert
2018-09-13Elaboration: do not ask small inductives to be templateGaëtan Gilbert
This doesn't change behaviour currently as the kernel also makes this decision, but in the future it won't.
2018-09-13Small simplification of elaboration side of template poly inductivesGaëtan Gilbert
2018-09-13Mention PRINT_LOGS=1 when failing test suiteGaëtan Gilbert
It seems people don't always look at the test suite readme.
2018-09-13Move test suite report script to standalone script fileGaëtan Gilbert
This allows for nicer formatting without having to deal with Make's semantic whitespace.
2018-09-13Merge PR #8467: Manual: fix documentation of the “fresh” tacticThéo Zimmermann
2018-09-13Merge PR #8470: Fix mli-doc following #7109.Maxime Dénès
2018-09-12Fix mli-doc following #7109.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 11:01:02 +0000