aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-06-13Revert "[travis] temporary UniMath overlay"Théo Zimmermann
This reverts commit 7ca4e36af8a12236a618bd3a8d045439df40dd43. Not necessary anymore since UniMath/UniMath#715 has been merged.
2017-06-13Merge PR#714: Print feature Proof-of-Concept (episode 2)Maxime Dénès
2017-06-13Merge PR#757: Better sectioning on travis log printing in test-suiteMaxime Dénès
2017-06-13Merge PR#743: Update .gitignoreMaxime Dénès
2017-06-13Merge PR#764: Point ci-hott at a newer version of HoTTMaxime Dénès
2017-06-13Merge PR#772: Store plugins/micromega/micromega.{ml,mli} files in the ↵Maxime Dénès
repository. Try to generate them later.
2017-06-12Store plugins/micromega/micromega.{ml,mli} files in the repository. Try to ↵Matej Košík
generate them later.
2017-06-12Merge PR#715: Add coq-dpdgraph ciMaxime Dénès
2017-06-12Merge PR#709: Bytecode compilation apart from 'make world', againMaxime Dénès
2017-06-12Merge PR#718: API cleanup: aliasesMaxime Dénès
2017-06-12Temporary overlay, waiting for upstream PR merges.Maxime Dénès
2017-06-12Merge PR#707: add support for "-bypass-API" argument to "coq_makefile"Maxime Dénès
2017-06-12add overlaysMatej Košík
2017-06-12Add support for "-bypass-API" argument of "coq_makefile"Matej Košík
Plugin-writers can now use: -bypass-API parameter with "coq_makefile". The effect of that is that instead of -I API the plugin will be compiled with: -I config" -I dev -I lib -I kernel -I library -I engine -I pretyping -I interp -I parsing -I proofs -I tactics -I toplevel -I printing -I intf -I grammar -I ide -I stm -I vernac
2017-06-12make test-suite/save-logs.sh usable also on old MacOS XMaxime Denes
2017-06-11Point ci-hott at a newer version of HoTTJason Gross
2017-06-10Remove remaining vo.itarget files (obsolete since PR #499)Pierre Letouzey
2017-06-10Fix Travis sectioningJason Gross
It drops anything after a `/`, so we change all `/`s into `.`. There must be a better way to do this that doesn't involve so much bash hackery, right?
2017-06-10Remove (useless) aliases from the API.Matej Košík
2017-06-09Better sectioning on travis log printing in test-suiteJason Gross
2017-06-09Makefile.common: remove an obsolete comment after PR#499Pierre Letouzey
2017-06-08Mirror dpdgraph's travis test more accuratelyJason Gross
2017-06-08Remove coq-dpdgraph overlayJason Gross
2017-06-08Merge branch 'v8.6'Pierre-Marie Pédrot
2017-06-08Remove overlay.Maxime Dénès
2017-06-08Merge PR#652: Put all plugins behind an "API".Maxime Dénès
2017-06-07Update .gitignoreJason Gross
2017-06-07add overlaysMatej Košík
2017-06-07Put "ssreflect" behind "API".Matej Košík
2017-06-07Put all plugins behind an "API".Matej Kosik
2017-06-07Merge PR#698: Trunk miscMaxime Dénès
2017-06-07Merge PR#717: [proof] Deprecate "proof mode" APIMaxime Dénès
2017-06-07Merge PR#669: Ssr mergeMaxime Dénès
2017-06-06Overlay.Maxime Dénès
2017-06-06Merge the ssr plugin.Maxime Dénès
2017-06-06Remove some overlays.Maxime Dénès
2017-06-06Merge PR#623: Remove the Sigma (monotonous state) API.Maxime Dénès
2017-06-06Overlays.Maxime Dénès
2017-06-06Remove the Sigma (monotonous state) API.Maxime Dénès
Reminder of (some of) the reasons for removal: - Despite the claim in sigma.mli, it does *not* prevent evar leaks, something like: fun env evd -> let (evd',ev) = new_evar env evd in (evd,ev) will typecheck even with Sigma-like type annotations (with a proof of reflexivity) - The API stayed embryonic. Even typing functions were not ported to Sigma. - Some unsafe combinators (Unsafe.tclEVARS) were replaced with slightly less unsafe ones (e.g. s_enter), but those ones were not marked unsafe at all (despite still being so). - There was no good story for higher order functions manipulating evar maps. Without higher order, one can most of the time get away with reusing the same name for the updated evar map. - Most of the code doing complex things with evar maps was using unsafe casts to sigma. This code should be fixed, but this is an orthogonal issue. Of course, this was showing a nice and elegant use of GADTs, but the cost/benefit ratio in practice did not seem good.
2017-06-06Merge PR#662: Fixing bug #5233 and another bug with implicit arguments + a ↵Maxime Dénès
short econstr-cleaning of record.ml
2017-06-06Merge PR#728: A few typos.Maxime Dénès
2017-06-06Merge PR#600: Some factorizations of ltac interpretation functions between ↵Maxime Dénès
ssreflect and coq code
2017-06-06Merge PR#638: Fix bug #5360: anomalies in typeclass resolution outputMaxime Dénès
2017-06-06Merge PR#716: Don't double up on periods in anomaliesMaxime Dénès
2017-06-06Merge PR#723: [travis] [fiat] Test also fiat-core.Maxime Dénès
2017-06-05Merge PR#724: Move README.ci to markdownMaxime Dénès
2017-06-05Merge PR#726: [stm] Solve bug 5577 "STM branch name is incorrect with Time"Maxime Dénès
2017-06-05Merge PR#722: [printing] Remove duplicated printing function.Maxime Dénès
2017-06-05Merge PR#590: A more explicit algebraic type for evars of kind MatchingVar + ↵Maxime Dénès
a flag suspectingly renamed in a clearer way
2017-06-04Added support for a side effect on constants in reduction functions.Thomas Sibut-Pinote
This exports two functions: - declare_reduction_effect: to declare a hook to be applied when some constant are visited during the execution of some reduction functions (primarily cbv, but also cbn, simpl, hnf, ...). - set_reduction_effect: to declare a constant on which a given effect hook should be called. Developed jointly by Thomas Sibut-Pinote and Hugo Herbelin. Added support for printing effect in functions of tacred.ml.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 17:27:28 +0000