aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-03-06Merge PR #6824: Remove deprecated options related to typeclasses.Maxime Dénès
2018-03-06Merge PR #6900: [compat] Remove "Tactic Pattern Unification"Maxime Dénès
2018-03-06Merge PR #6898: [compat] Remove "Intuition Iff Unfolding"Maxime Dénès
2018-03-06Merge PR #6901: [compat] Remove "Injection L2R Pattern Order"Maxime Dénès
2018-03-05[coq] Adapt to correct LTAC module packing coq/coq#6869Emilio Jesus Gallego Arias
2018-03-05[toplevel] Modify printing goal strategy.Emilio Jesus Gallego Arias
Instead of using a command-analysis heuristic, coqtop will now print goals if the goal has changed. We use a fast goal comparison heuristic, but a more refined strategy would be possible. This brings some [IMHO very welcome] change to PG and `-emacs`, which will now disable the printing of goals. Now, instead of playing with `Set/Unset Silent` and a bunch of other hacks, PG can issue a `Show` command whenever it wishes to redisplay the goals. This change will break PG, so we need to carefully coordinate this PR with PG upstream (see ProofGeneral/PG#212). Some interesting further things to do: - Detect changes in nested proofs. - Uncouple the silent flag from "print goals".
2018-03-05Fix failing packaging job.Théo Zimmermann
gtksourceview depends transitively on py2cairo which was updated in Homebrew to depend explicitly on python2 (see Homebrew/homebrew-core#24714): this makes the python3 install step impossible. We also remove the libxml2 install step which was failing in a non-fatal way.
2018-03-05Remove NOPLUGINDOCS optionmrmr1993
2018-03-05Add empty description for @raise statements to satisfy ocamldocmrmr1993
2018-03-05Escape curly braces in ocamldoc commentmrmr1993
2018-03-05Separate vim/emacs fold markers from ocamldoc commentsmrmr1993
ocamldoc chokes on the markers {{{ and }}} because { and } are part of its syntax
2018-03-05Build docs for plugins by default, add NOPLUGINDOCS flag to disablemrmr1993
2018-03-05Change non-documentation comment from ocamldoc stylemrmr1993
2018-03-05Fix formatting of some ocamldoc comments to reduce warningsmrmr1993
2018-03-05Replace invalid tag @raises in ocamldoc comments with @raisemrmr1993
2018-03-05Remove non-existent dependencymrmr1993
2018-03-05Tweak comments to fix ocamldoc errorsmrmr1993
2018-03-05Tidy up ml-doc outut, give it a separate output directorymrmr1993
2018-03-05Use computed deps to generate ml-doc and use implicit mli-doc depsmrmr1993
2018-03-05[build] Simpler byte/opt toplevel build.Emilio Jesus Gallego Arias
Instead of playing static linking games, we just ship two different top-level files depending on whether we want to enable `Drop` support [bytecode case] or not. The savings of the old approach [1 line of code] were not worth the complexities of the linking hack.
2018-03-05CHANGES and tests for with Definition @{univs}Gaëtan Gilbert
2018-03-05Allow universe declarations for [with Definition].Gaëtan Gilbert
2018-03-05Deprecate Focus and Unfocus.Théo Zimmermann
2018-03-05[ssreflect] Export parsing witnesses in mli file.Emilio Jesus Gallego Arias
This is needed in order to manipulate/serialize SSR's AST. A quicker [and maybe better] alternative would be to just remove `ssrparser.mli`, as there are many grammar entries that still need exporting.
2018-03-05Sanitize universe declaration in Context (stop using a ref...)Gaëtan Gilbert
When there is more than one variable to declare we stop trying to attach global universes (ie monomorphic or section polymorphic) to one of them.
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-05configure: -warn-error: now takes a bool so that you can also turn it offEnrico Tassi
2018-03-05configure: profiles (sets of flags)Enrico Tassi
2018-03-05configure: make Prefs a record rather than a module of refsEnrico Tassi
In this way it is easy to support multiple defaults
2018-03-05Merge PR #6700: [ssr] rewrite Ssripats and Ssrview in the tactic monadMaxime Dénès
2018-03-04[compat] Remove NOOP and alias deprecated options.Emilio Jesus Gallego Arias
Following up on #6791, we remove: - `Record Elimination Schemes`, a deprecated alias of `Nonrecursive Elimination Schemes` - `Match Strict` a deprecated NOOP.
2018-03-04Remove deprecated options related to typeclasses.Théo Zimmermann
2018-03-04ssr: add Prenex Implicits for Some_inj to use it as a viewAnton Trunov
2018-03-04ssr: fix typo in doc commentAnton Trunov
2018-03-04Merge PR #935: Handling evars in the VMMaxime Dénès
2018-03-04ssr: ipats: V82.tactic ~nf_evars:false everywhereEnrico Tassi
2018-03-04Proofview: V82.tactic option to not normalize evarsEnrico Tassi
2018-03-04ssr: rewrite Ssripats and Ssrview in the tactic monadEnrico Tassi
Ssripats and Ssrview are now written in the Tactic Monad. Ssripats implements the => tactical. Ssrview implements the application of forward views. The code is, according to my tests, 100% backward compatible. The code is much more documented than before. Moreover the "ist" (ltac context) used to interpret views is the correct one (the one at ARGUMENT EXTEND interp time, not the one at TACTIC EXTEND execution time). Some of the code not touched by this commit still uses the incorrect ist, so its visibility in TACTIC EXTEND can't be removed yet. The main changes in the code are: - intro patterns are implemented using a state machine (a goal comes with a state). Ssrcommon.MakeState provides an easy way for a tactic to enrich the goal with with data of interest, such as the set of hyps to be cleared. This cleans up the old implementation that, in order to thread the state, that to redefine a bunch of tclSTUFF - the interpretation of (multiple) forward views uses the state to accumulate intermediate results - the bottom of Sscommon collects a bunch of utilities written in the tactic monad. Most of them are the rewriting of already existing utilities. When possible the old version was removed.
2018-03-04tactics: export e_reduct_in_conclEnrico Tassi
2018-03-04reductionops: remove dead code "bind_assum"Enrico Tassi
2018-03-04proofview: debug API to print a goalEnrico Tassi
2018-03-04Merge PR #6791: Removing compatibility support for versions older than 8.5.Maxime Dénès
2018-03-04Merge PR #6736: [toplevel] Move beautify to its own pass.Maxime Dénès
2018-03-04Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.Maxime Dénès
2018-03-04Merge PR #6876: Unify Const_sorts and Const_type, and remove VsortMaxime Dénès
2018-03-04Merge PR #6846: Moving code for "simple induction"/"simple destruct" to ↵Maxime Dénès
coretactics.ml4.
2018-03-04Merge PR #6885: [stm] Partial fix for bug #6884 [location missing from ↵Maxime Dénès
replay nodes]
2018-03-04Merge PR #6873: [toplevel] Update state when `Drop` exception is thrown [#6872]Maxime Dénès
2018-03-04Merge PR #6882: Harden gitattributes against core.whitespace configuration.Maxime Dénès
2018-03-04Merge PR #6879: Fix #6878: univ undefined for [with Definition] bad instance ↵Maxime Dénès
size.
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-28 11:07:29 +0000