aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-09-19Fix Numeral Notations (2/4 - exceptions, usr_err)Jason Gross
2018-09-19Fix Numeral Notations (1/4 - moving things)Jason Gross
2018-09-19Merge PR #8505: Fix Windows builds: OPAM has changed its URL schema.Michael Soegtrop
2018-09-19Merge PR #8246: Implementing an internal basic version of the "pose" tactic i...Enrico Tassi
2018-09-19[ssr] use the right environment in ssrpattern (fix #8454)Enrico Tassi
2018-09-19Fix Windows builds: OPAM has changed its URL schema.Théo Zimmermann
2018-09-19Merge PR #7343: Add missing index entries.Maxime Dénès
2018-09-19Fix #7754: universe declarations on mutual inductivesGaëtan Gilbert
2018-09-19Replace trivial uses of declare_summary with summary.refsGaëtan Gilbert
2018-09-19Remove Hints.add_hints_initGaëtan Gilbert
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 unif...Pierre-Marie Pédrot
2018-09-19Merge PR #8447: Cleaning in the retroknowledgePierre-Marie Pédrot
2018-09-19Merge PR #8463: Remove DischargedhypsmapsPierre-Marie Pédrot
2018-09-18[api] Deprecate two forgotten print functions that use global state.Emilio Jesus Gallego Arias
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-18Zify: replace local definitions by equationsVincent Laporte
2018-09-18Removing Dischargedhypsmap which is unused internally.Maxime Dénès
2018-09-17Add missing index entries.Théo Zimmermann
2018-09-17Ensure_prev_proof returns a proof that has underlying differences fromJim Fehrle
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
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
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
2018-09-13Add doc for template polymorphism option and attributes.Gaëtan Gilbert