aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-06-11A stronger test that #use"include";; works well.Hugo Herbelin
2017-06-11Fixing base_include after loc is an option (30d3515).Hugo Herbelin
2017-06-11Normalize deprecation notices of ./configureThéo Zimmermann
Always output a warning on stderr when a deprecated option is used.
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-10don't leak unqualified identifiers from the macroMatej Košík
2017-06-10Remove (useless) aliases from the API.Matej Košík
2017-06-10[toplevel] Print error header on fatal batch error.Emilio Jesus Gallego Arias
2017-06-09Better sectioning on travis log printing in test-suiteJason Gross
2017-06-09Fix Bug #5568, no dup notation warnings on repeated module importsPaul Steckler
2017-06-09A fix to #5414 (ident bound by ltac names now known for "match").Hugo Herbelin
Also taking into account a name in the return clause and in the indices. Note the double meaning ``bound as a term to match'' and ``binding in the "as" clause'' when the term to match is a variable for all of "match", "if" and "let".
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-08Fix bug 5026 (the stdlib shouldn't define inconsistent notations).Théo Zimmermann
2017-06-08Merge branch 'v8.6'Pierre-Marie Pédrot
2017-06-08Adding a test case as requested in bug 5205.Théo Zimmermann
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-07[stm] More fixes for nested commands [bugzilla 5589]Emilio Jesus Gallego Arias
2017-06-07Fix documentation of Typeclasses eauto :=Théo Zimmermann
2017-06-07completing a sentence in a commentMatej Košík
2017-06-07[kernel] Improve proof using message, fixes bugzilla #3613Emilio Jesus Gallego Arias
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-05Univs: fix bug #5365, generation of u+k <= v constraintsMatthieu Sozeau
Use an explicit label ~algebraic for make_flexible_variable as well.
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.
2017-06-04A few typos.Hugo Herbelin
2017-06-04Ensure that warnings new from ocaml > 4.01 remains silent.Hugo Herbelin
Indeed, 8.6 is announced to be compilable with 4.01.0 and it is convenient not seeing warnings about which nothing can be done. Remove deprecation warnings new from ocaml 4.03, as well as warning 52. This is a partial cherry-pick of a77734ad6.
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-19 21:27:21 +0000