aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-08-01Improved grammar and spelling for chapters 'Utilities' and 'CoqIDE' of the Re...Zeimer
2018-07-27Merge PR #8173: Missing backslash in a documentation file.Théo Zimmermann
2018-07-27Missing backslash in the documentation file.Martin Bodin
2018-07-27Merge PR #8164: Add information to option type errorsEnrico Tassi
2018-07-27Merge PR #8166: Fix Search query in CoqIDE.Enrico Tassi
2018-07-27Merge PR #8103: Coercions cleanup: use GlobRef.t instead of constrEnrico Tassi
2018-07-27Merge PR #8141: Diff option in CoqIDEEnrico Tassi
2018-07-26Merge PR #8101: Remove ClosedModule and ClosedSection from libstackEnrico Tassi
2018-07-26Fix Search query in CoqIDE.Pierre-Marie Pédrot
2018-07-26Add information to option type errorsTej Chajed
2018-07-26Replace iter + ref by fold_leftMaxime Dénès
2018-07-26restore reduction of coercion to eventually expose a constructorEnrico Tassi
2018-07-26Coercions cleanup: use GlobRef.t instead of constrMaxime Dénès
2018-07-26Merge PR #8100: Use just one object declaration for all global universe addit...Pierre-Marie Pédrot
2018-07-26Merge PR #8050: Cleanup VERNAC EXTENDMaxime Dénès
2018-07-26Expose the diff printing option as an UI entry in CoqIDE.Pierre-Marie Pédrot
2018-07-26Do not set diff printing on by default in CoqIDE.Pierre-Marie Pédrot
2018-07-26Merge PR #8122: Fix #8119: anomalies in vm_compute with let and evars.Maxime Dénès
2018-07-26Merge PR #7786: In "redundant clause" pattern-matching error, show also the p...Pierre-Marie Pédrot
2018-07-26Merge PR #8084: Properly disable native compilation when -native-compiler is ...Maxime Dénès
2018-07-26Merge PR #7274: Avoiding introducing dependency on the indices of a term whic...Pierre-Marie Pédrot
2018-07-26Merge PR #8150: Fix static declaration of plugins in coqpp.Emilio Jesus Gallego Arias
2018-07-25Remove object duplication for Constraint command.Gaëtan Gilbert
2018-07-25Hints use Declare to declare universes instead of a custom object.Gaëtan Gilbert
2018-07-25Merge PR #7859: Remove himsg.pr_puniverses, use @{} for universe printing in ...Pierre-Marie Pédrot
2018-07-25Merge PR #8133: Fixes #8126: issue with notations and nested applicationsEmilio Jesus Gallego Arias
2018-07-25Merge PR #734: [travis] Also run coqchk on HoTTEmilio Jesus Gallego Arias
2018-07-25In "redundant clause" pattern-matching error, show also the pattern (#7777).Hugo Herbelin
2018-07-25Optimized dependencies for pattern-matching on only trivial patterns.Hugo Herbelin
2018-07-25Fix static declaration of plugins in coqpp.Pierre-Marie Pédrot
2018-07-25Add overlay for EquationsGaëtan Gilbert
2018-07-25Remove himsg.pr_puniverses, use @{} for universe printing in errorsMaxime Dénès
2018-07-25Merge PR #7889: Cleanup reduction effects: they only work on constants.Pierre-Marie Pédrot
2018-07-25Merge PR #8139: Replace all the CoInductives with Variants in the SSR pluginEnrico Tassi
2018-07-25Merge PR #8063: Direct implementation of Ascii.eqb and String.eqb (take 2)Hugo Herbelin
2018-07-25Replace all the CoInductives with Variants in the SSR pluginKazuhiko Sakaguchi
2018-07-24[travis] Also run coqchk on HoTTJason Gross
2018-07-24Merge PR #7908: Projections use index representationPierre-Marie Pédrot
2018-07-24Fix #8119: anomalies in vm_compute with let and evars.Pierre-Marie Pédrot
2018-07-24Add combinators to drop the bodies of local declarations.Pierre-Marie Pédrot
2018-07-24Properly disable native compilation when -native-compiler is unset.Pierre-Marie Pédrot
2018-07-24Merge PR #8040: [ci] Enable native compiler in `egde:flambda` build.Gaëtan Gilbert
2018-07-24Add simple test cases for vm and native on primitive projections.Gaëtan Gilbert
2018-07-24VM: don't duplicate projection narg information in lproj/kprojGaëtan Gilbert
2018-07-24Add overlay for Equations.Gaëtan Gilbert
2018-07-24Fix #7329: coqchk Include with primitive projectionsGaëtan Gilbert
2018-07-24Projections use index representationGaëtan Gilbert
2018-07-24Fixes #8126 (issue with notations and nested applications).Hugo Herbelin
2018-07-24Remove useless is_projection in tacredGaëtan Gilbert
2018-07-24Move Heads to pretyping (is_projection will move to Recordops)Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-02 05:40:24 +0000