aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Collapse)Author
2017-12-15Merge PR #6219: Document undocumented optionsMaxime Dénès
2017-12-14Deprecate dead option Match Strict (ssr).Gaëtan Gilbert
2017-12-14Deprecate dead code option Congruence Depth.Gaëtan Gilbert
2017-12-14Merge PR #6386: Catch errors while coercing 'and' intro patternsMaxime Dénès
2017-12-14Merge PR #6116: ssr: fill_occ_pattern: return valid ustate even if no match ↵Maxime Dénès
(fix #6106)
2017-12-14Merge PR #6379: Fix profiling pluginMaxime Dénès
2017-12-14Merge PR #978: In printing, experimenting factorizing "match" clauses with ↵Maxime Dénès
same right-hand side.
2017-12-14Merge PR #6169: Clean up/deprecated optionsMaxime Dénès
2017-12-14Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.Maxime Dénès
2017-12-12In printing, factorizing "match" clauses with same right-hand side.Hugo Herbelin
Moreover, when there are at least two clauses and the last most factorizable one is a disjunction with no variables, turn it into a catch-all clause. Adding options Unset Printing Allow Default Clause. to deactivate the second behavior, and Unset Printing Factorizable Match Patterns. to deactivate the first behavior (deactivating the first one deactivates also the second one). E.g. printing match x with Eq => 1 | _ => 0 end gives match x with | Eq => 1 | _ => 0 end or (with default clause deactivates): match x with | Eq => 1 | Lt | Gt => 0 end More to be done, e.g. reconstructing multiple patterns in Nat.eqb...
2017-12-12Removing cumbersome location in multiple patterns.Hugo Herbelin
This is to have a better symmetry between CCases and GCases.
2017-12-11Use msg_info for LtacProfJason Gross
This way, `Time Show Ltac Profile` shows the profile in `*response*` in PG, without an extra `infomsg` tag on the timing.
2017-12-11Allow LtacProf tactics to be calledJason Gross
This fixes #6378. Previously the ML module was never declared anywhere. Thanks to @cmangin for the pointer.
2017-12-11Catch errors while coercing 'and' intro patternsTej Chajed
Fixes GH#6384 and GH#6385.
2017-12-11[proof] Embed evar_map in RefinerError exception.Emilio Jesus Gallego Arias
The exception needs to carry aroud a pair of `env, sigma` so printing is correct. This gets rid of a few global calls, and it is IMO the right thing to do. While we are at it, we incorporate some fixes to a couple of additional printing functions missing the `env, sigma` pair.
2017-12-11Remove deprecated appcontext and corresponding documentation.Théo Zimmermann
2017-12-11Remove deprecated option Tactic Compat Context.Théo Zimmermann
And some code simplification.
2017-12-11Merge PR #6324: Fix #6323: stronger restrict universe context vs abstract.Maxime Dénès
2017-12-11Merge PR #1150: [stm] Remove all but one use of VtUnknown.Maxime Dénès
2017-12-11Merge PR #6338: Remove up-to-conversion term matchingMaxime Dénès
2017-12-09[lib] Rename Profile to CProfileEmilio Jesus Gallego Arias
New module introduced in OCaml 4.05 I think, can create problems when linking with the OCaml toplevel for `Drop`.
2017-12-09[stm] Remove all but one use of VtUnknown.Emilio Jesus Gallego Arias
Together with #1122, this makes `VernacInstance` the only command in the Coq codebase that cannot be statically determined to open a proof. The reasoning for the commands moved to `VtSideff` is that parser-altering commands should be always marked `VtNow`; the rest can be usually marked as `VtLater`.
2017-12-08Merge PR #6158: Allows a level in the raw and glob printersMaxime Dénès
2017-12-07Merge PR #6322: Fix #6286 (non stability of micromega csdp cache rebuilding)Maxime Dénès
2017-12-06Getting rid of pf_is_matching in Funind.Pierre-Marie Pédrot
2017-12-06Fix #6323: stronger restrict universe context vs abstract.Gaëtan Gilbert
In the test we do [let X : Type@{i} := Set in ...] with Set abstracted. The constraint [Set < i] was lost in the abstract. Universes of a monomorphic reference [c] are considered to appear in the term [c].
2017-12-05Replacing Hashtbl.add by Hashtbl.replace in micromega cache building.Hugo Herbelin
This fixes #6286 as suggested by PMP. See details of discussion at #6286.
2017-12-05Merge PR #890: Global universe declarationsMaxime Dénès
2017-12-05Merge PR #6220: Use OCaml criteria for infix ops in extraction, #6212Maxime Dénès
2017-12-05Merge PR #6210: More complete not-fully-applied error messages, #6145Maxime Dénès
2017-12-01Proper nametab handling of global universe namesMatthieu Sozeau
They are now bound at the library + module level and can be qualified and shadowed according to the usual rules of qualified names. Parsing and printing of universes "u+n" done as well. In sections, global universes are discharged as well, checking that they can be defined globally when they are introduced
2017-11-29Remove "obsolete_locality" and fix STM vernac classification.Maxime Dénès
We remove deprecated syntax "Coercion Local" and such, and seize the opportunity to refactor some code around vernac_expr. We also do a small fix on the STM classification, which didn't know about Let Fixpoint and Let CoFixpoint. This is a preliminary step for the work on attributes.
2017-11-28more complete not-fully-applied error messages, #6145Paul Steckler
2017-11-28Merge PR #1033: Universe binder improvementsMaxime Dénès
2017-11-28Merge PR #6248: [api] Remove aliases of `Evar.t`Maxime Dénès
2017-11-27allow :: and , as infix opsPaul Steckler
2017-11-26[api] Remove aliases of `Evar.t`Emilio Jesus Gallego Arias
There don't really bring anything, we also correct some minor nits with the printing function.
2017-11-24Use Evarutil.has_undefined_evars for tactic has_evar.Gaëtan Gilbert
2017-11-24Use Entries.constant_universes_entry more.Gaëtan Gilbert
This reduces conversions between ContextSet/UContext and encodes whether we are polymorphic by which constructor we use rather than using some boolean.
2017-11-24When declaring constants/inductives use ContextSet if monomorphic.Gaëtan Gilbert
Also use constant_universes_entry instead of a bool flag to indicate polymorphism in ParameterEntry. There are a few places where we convert back to ContextSet because check_univ_decl returns a UContext, this could be improved.
2017-11-24Stop exposing UState.universe_context and its Evd wrapper.Gaëtan Gilbert
We can enforce properties through check_univ_decl, or get an arbitrary ordered context with UState.context / Evd.to_universe_context (the later being a new wrapper of the former).
2017-11-24Separate checking univ_decls and obtaining universe binder names.Gaëtan Gilbert
2017-11-24Extending further PR#6047 (system to register printers for Ltac values).Hugo Herbelin
We generalize the possible use of levels to raw and glob printers. This is potentially useful for printing ltac expressions which are the glob level.
2017-11-24Printing again "intros **" as "intros" by default.Hugo Herbelin
The rationale it that it is more common to do so and thus more "natural" (principle of writing less whenever possible).
2017-11-24Merge PR #6205: Fixing a 8.7 regression of ring_simplify in ArithRingMaxime Dénès
2017-11-24Merge PR #486: Make some functions on terms more robust w.r.t new term ↵Maxime Dénès
constructs.
2017-11-24Merge PR #876: In omega or romega, recognizing Z and nat modulo conversionMaxime Dénès
2017-11-24Merge PR #6197: [plugin] Remove LocalityFixme über hack.Maxime Dénès
2017-11-23Make some functions on terms more robust w.r.t new term constructs.Maxime Dénès
Extending terms is notoriously difficult. We try to get more help from the compiler by making sure such an extension will trigger non exhaustive pattern matching warnings.
2017-11-23Merge PR #6186: [api] Miscellaneous consolidation.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-10 17:23:34 +0000