aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Collapse)AuthorAge
* Merge PR #978: In printing, experimenting factorizing "match" clauses with ↵Gravatar Maxime Dénès2017-12-14
|\ | | | | | | same right-hand side.
* \ Merge PR #6169: Clean up/deprecated optionsGravatar Maxime Dénès2017-12-14
|\ \
* \ \ Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.Gravatar Maxime Dénès2017-12-14
|\ \ \
| | | * In printing, factorizing "match" clauses with same right-hand side.Gravatar Hugo Herbelin2017-12-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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...
| | | * Removing cumbersome location in multiple patterns.Gravatar Hugo Herbelin2017-12-12
| | | | | | | | | | | | | | | | This is to have a better symmetry between CCases and GCases.
* | | | [proof] Embed evar_map in RefinerError exception.Gravatar Emilio Jesus Gallego Arias2017-12-11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | * | Remove deprecated appcontext and corresponding documentation.Gravatar Théo Zimmermann2017-12-11
| | | |
| | * | Remove deprecated option Tactic Compat Context.Gravatar Théo Zimmermann2017-12-11
| |/ / |/| | | | | | | | And some code simplification.
* | | Merge PR #6324: Fix #6323: stronger restrict universe context vs abstract.Gravatar Maxime Dénès2017-12-11
|\ \ \
* \ \ \ Merge PR #1150: [stm] Remove all but one use of VtUnknown.Gravatar Maxime Dénès2017-12-11
|\ \ \ \
* \ \ \ \ Merge PR #6338: Remove up-to-conversion term matchingGravatar Maxime Dénès2017-12-11
|\ \ \ \ \ | |_|_|_|/ |/| | | |
| | | | * [lib] Rename Profile to CProfileGravatar Emilio Jesus Gallego Arias2017-12-09
| |_|_|/ |/| | | | | | | | | | | | | | | New module introduced in OCaml 4.05 I think, can create problems when linking with the OCaml toplevel for `Drop`.
| | * | [stm] Remove all but one use of VtUnknown.Gravatar Emilio Jesus Gallego Arias2017-12-09
| |/ / |/| | | | | | | | | | | | | | | | | | | | | | | 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`.
* | | Merge PR #6158: Allows a level in the raw and glob printersGravatar Maxime Dénès2017-12-08
|\ \ \
* \ \ \ Merge PR #6322: Fix #6286 (non stability of micromega csdp cache rebuilding)Gravatar Maxime Dénès2017-12-07
|\ \ \ \
| | | * | Getting rid of pf_is_matching in Funind.Gravatar Pierre-Marie Pédrot2017-12-06
| |_|/ / |/| | |
| | | * Fix #6323: stronger restrict universe context vs abstract.Gravatar Gaëtan Gilbert2017-12-06
| |_|/ |/| | | | | | | | | | | | | | | | | | | | 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].
| * | Replacing Hashtbl.add by Hashtbl.replace in micromega cache building.Gravatar Hugo Herbelin2017-12-05
| | | | | | | | | | | | This fixes #6286 as suggested by PMP. See details of discussion at #6286.
* | | Merge PR #890: Global universe declarationsGravatar Maxime Dénès2017-12-05
|\ \ \
* \ \ \ Merge PR #6220: Use OCaml criteria for infix ops in extraction, #6212Gravatar Maxime Dénès2017-12-05
|\ \ \ \
* \ \ \ \ Merge PR #6210: More complete not-fully-applied error messages, #6145Gravatar Maxime Dénès2017-12-05
|\ \ \ \ \ | |_|_|/ / |/| | | |
| | | * | Proper nametab handling of global universe namesGravatar Matthieu Sozeau2017-12-01
| |_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* | | | Remove "obsolete_locality" and fix STM vernac classification.Gravatar Maxime Dénès2017-11-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| * | | more complete not-fully-applied error messages, #6145Gravatar Paul Steckler2017-11-28
| | | |
* | | | Merge PR #1033: Universe binder improvementsGravatar Maxime Dénès2017-11-28
|\ \ \ \
* \ \ \ \ Merge PR #6248: [api] Remove aliases of `Evar.t`Gravatar Maxime Dénès2017-11-28
|\ \ \ \ \
| | | | * | allow :: and , as infix opsGravatar Paul Steckler2017-11-27
| | | | | |
| * | | | | [api] Remove aliases of `Evar.t`Gravatar Emilio Jesus Gallego Arias2017-11-26
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | There don't really bring anything, we also correct some minor nits with the printing function.
* | | | | | Use Evarutil.has_undefined_evars for tactic has_evar.Gravatar Gaëtan Gilbert2017-11-24
|/ / / / /
| * | | | Use Entries.constant_universes_entry more.Gravatar Gaëtan Gilbert2017-11-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This reduces conversions between ContextSet/UContext and encodes whether we are polymorphic by which constructor we use rather than using some boolean.
| * | | | When declaring constants/inductives use ContextSet if monomorphic.Gravatar Gaëtan Gilbert2017-11-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| * | | | Stop exposing UState.universe_context and its Evd wrapper.Gravatar Gaëtan Gilbert2017-11-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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).
| * | | | Separate checking univ_decls and obtaining universe binder names.Gravatar Gaëtan Gilbert2017-11-24
|/ / / /
| | | * Extending further PR#6047 (system to register printers for Ltac values).Gravatar Hugo Herbelin2017-11-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | * Printing again "intros **" as "intros" by default.Gravatar Hugo Herbelin2017-11-24
| |_|/ |/| | | | | | | | | | | The rationale it that it is more common to do so and thus more "natural" (principle of writing less whenever possible).
* | | Merge PR #6205: Fixing a 8.7 regression of ring_simplify in ArithRingGravatar Maxime Dénès2017-11-24
|\ \ \
* \ \ \ Merge PR #486: Make some functions on terms more robust w.r.t new term ↵Gravatar Maxime Dénès2017-11-24
|\ \ \ \ | | | | | | | | | | | | | | | constructs.
* \ \ \ \ Merge PR #876: In omega or romega, recognizing Z and nat modulo conversionGravatar Maxime Dénès2017-11-24
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6197: [plugin] Remove LocalityFixme über hack.Gravatar Maxime Dénès2017-11-24
|\ \ \ \ \ \
| | | * | | | Make some functions on terms more robust w.r.t new term constructs.Gravatar Maxime Dénès2017-11-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | | | | Merge PR #6186: [api] Miscellaneous consolidation.Gravatar Maxime Dénès2017-11-23
|\ \ \ \ \ \ \ | |_|_|/ / / / |/| | | | | |
| | | * | | | Recognizing Z in romega up to conversion.Gravatar Hugo Herbelin2017-11-23
| | | | | | |
| | | * | | | Using is_conv rather than eq_constr to find `nat` or `Z` in omega.Gravatar Hugo Herbelin2017-11-23
| |_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Moving at the same to a passing "env sigma" style rather than passing "gl". Not that it is strictly necessary, but since we had to move functions taking only a "sigma" to functions taking also a "env", we eventually adopted the "env sigma" style. (The "gl" style would have been as good.) This answers wish #4717.
| | | * | | Fixing a 8.7 regression of ring_simplify in ArithRing.Gravatar Hugo Herbelin2017-11-23
| |_|/ / / |/| | | | | | | | | | | | | | | | | | | With help from Guillaume (see discussion at https://github.com/coq/coq/issues/6191).
* | | | | Merge PR #6192: Fix #5790: make Hint Resolve <- respect univ polymorphism flag.Gravatar Maxime Dénès2017-11-23
|\ \ \ \ \
| | | * | | [plugin] Remove LocalityFixme über hack.Gravatar Emilio Jesus Gallego Arias2017-11-22
| |_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | To that extent we introduce a new prototype vernacular extension macro `VERNAC COMMAND FUNCTIONAL EXTEND` that will take a function with the proper parameters and attributes. This of course needs more refinement, in particular we should move `vernac_command` to its own file and make `Vernacentries` consistent wrt it.
| | | | * allow whitespace around infix opGravatar Paul Steckler2017-11-22
| | | | |
| | | | * use OCaml criteria for infix ops, #6212Gravatar Paul Steckler2017-11-22
| |_|_|/ |/| | |
| | * | [api] Deprecate Term destructors, move to ConstrGravatar Emilio Jesus Gallego Arias2017-11-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | We mirror the structure of EConstr and move the destructors from `Term` to `Constr`. This is a step towards having a single module for `Constr`.
| | * | [api] Miscellaneous consolidation + moves to engine.Gravatar Emilio Jesus Gallego Arias2017-11-21
| |/ / |/| | | | | | | | | | | | | | We deprecate a few functions that were deprecated in the comments plus we place `Nameops` and `Univops` in engine where they do seem to belong in the large picture of code organization.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-21 18:42:23 +0000