aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-26Improved chapters 'Implicit Coercions' and 'Canonical Structures' of the Refe...Zeimer
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-26Don't use an object for polymorphic section universesGaëtan Gilbert
2018-07-26Universe object is DisposeGaëtan Gilbert
2018-07-26Merge PR #8100: Use just one object declaration for all global universe addit...Pierre-Marie Pédrot
2018-07-26Fix #8121: anomalies in native_compute with let and evars.Pierre-Marie Pédrot
2018-07-26Adding an overlay for Mtac2.Pierre-Marie Pédrot
2018-07-26Turn the kernel reduction sharing flag into an argument passed in the cache.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-25Fix #7900 previous commit fixes a bug when using side effects in obligations.Matthieu Sozeau
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-25[sphinx] Add a way of skipping names in the indexes.Théo Zimmermann
2018-07-25kernel: missing check that all universes are declared.Matthieu Sozeau
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-25Doc: preliminary work before #7291 which add an "Unable to unify" message.Hugo Herbelin
2018-07-25[ssr] assertion -> error message (Fix #8134)Enrico Tassi
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-01 14:56:21 +0000