| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-12-08 | Merge PR #6158: Allows a level in the raw and glob printers | Maxime Dénès | |
| 2017-12-07 | Merge PR #6322: Fix #6286 (non stability of micromega csdp cache rebuilding) | Maxime Dénès | |
| 2017-12-05 | Replacing 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-05 | Merge PR #890: Global universe declarations | Maxime Dénès | |
| 2017-12-05 | Merge PR #6220: Use OCaml criteria for infix ops in extraction, #6212 | Maxime Dénès | |
| 2017-12-05 | Merge PR #6210: More complete not-fully-applied error messages, #6145 | Maxime Dénès | |
| 2017-12-01 | Proper nametab handling of global universe names | Matthieu 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-29 | Remove "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-28 | more complete not-fully-applied error messages, #6145 | Paul Steckler | |
| 2017-11-28 | Merge PR #1033: Universe binder improvements | Maxime Dénès | |
| 2017-11-28 | Merge PR #6248: [api] Remove aliases of `Evar.t` | Maxime Dénès | |
| 2017-11-27 | allow :: and , as infix ops | Paul 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-24 | Use Evarutil.has_undefined_evars for tactic has_evar. | Gaëtan Gilbert | |
| 2017-11-24 | Use 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-24 | When 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-24 | Stop 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-24 | Separate checking univ_decls and obtaining universe binder names. | Gaëtan Gilbert | |
| 2017-11-24 | Extending 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-24 | Printing 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-24 | Merge PR #6205: Fixing a 8.7 regression of ring_simplify in ArithRing | Maxime Dénès | |
| 2017-11-24 | Merge PR #486: Make some functions on terms more robust w.r.t new term ↵ | Maxime Dénès | |
| constructs. | |||
| 2017-11-24 | Merge PR #876: In omega or romega, recognizing Z and nat modulo conversion | Maxime Dénès | |
| 2017-11-24 | Merge PR #6197: [plugin] Remove LocalityFixme über hack. | Maxime Dénès | |
| 2017-11-23 | Make 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-23 | Merge PR #6186: [api] Miscellaneous consolidation. | Maxime Dénès | |
| 2017-11-23 | Recognizing Z in romega up to conversion. | Hugo Herbelin | |
| 2017-11-23 | Using is_conv rather than eq_constr to find `nat` or `Z` in omega. | Hugo Herbelin | |
| 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. | |||
| 2017-11-23 | Fixing a 8.7 regression of ring_simplify in ArithRing. | Hugo Herbelin | |
| With help from Guillaume (see discussion at https://github.com/coq/coq/issues/6191). | |||
| 2017-11-23 | Merge PR #6192: Fix #5790: make Hint Resolve <- respect univ polymorphism flag. | Maxime Dénès | |
| 2017-11-22 | [plugin] Remove LocalityFixme über hack. | Emilio Jesus Gallego Arias | |
| 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. | |||
| 2017-11-22 | allow whitespace around infix op | Paul Steckler | |
| 2017-11-22 | use OCaml criteria for infix ops, #6212 | Paul Steckler | |
| 2017-11-22 | [api] Deprecate Term destructors, move to Constr | Emilio Jesus Gallego Arias | |
| 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`. | |||
| 2017-11-21 | [api] Miscellaneous consolidation + moves to engine. | Emilio Jesus Gallego Arias | |
| 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. | |||
| 2017-11-21 | [printing] Deprecate all printing functions accessing the global proof. | Emilio Jesus Gallego Arias | |
| We'd like to handle proofs functionally we thus recommend not to use printing functions without an explicit context. We also adapt most of the code, making more explicit where the printing environment is coming from. An open task is to refactor some code so we gradually make the `Pfedit.get_current_context ()` disappear. | |||
| 2017-11-21 | Merge PR #6181: [proof] Attempt to deprecate some V82 parts of the proof API. | Maxime Dénès | |
| 2017-11-21 | Merge PR #6113: Extra work on ltac printing: fixing #5787, some parentheses | Maxime Dénès | |
| 2017-11-20 | Fixes #5787 (printing of "constr:" lost in the move of constr to Generic). | Hugo Herbelin | |
| Was broken since 8.6. | |||
| 2017-11-20 | Merge PR #6183: [plugins] Prepare plugin API for functional handling of state. | Maxime Dénès | |
| 2017-11-20 | Merge PR #6161: Fix micromega.ml to match generated file and enforce match ↵ | Maxime Dénès | |
| in make. | |||
| 2017-11-19 | Fix #5790: make Hint Resolve <- respect univ polymorphism flag. | Gaëtan Gilbert | |
| 2017-11-19 | [plugins] Prepare plugin API for functional handling of state. | Emilio Jesus Gallego Arias | |
| To this purpose we allow plugins to register functions that will modify the state. This is not used yet, but will be used soon when we remove the global handling of the proof state. | |||
| 2017-11-19 | [proof] Attempt to deprecate some V82 parts of the proof API. | Emilio Jesus Gallego Arias | |
| I followed what seems to be the intention of the code, with the original intention of remove the global imperative proof state. However, I fully fail to see why the new API is better than the old one. In fact the opposite seems the contrary. Still big parts of the "new proof engine" seem unfinished, and I'm afraid I am not the right person to know what direction things should take. | |||
| 2017-11-16 | Merge PR #6148: [api] Another large deprecation, `Nameops` and friends. | Maxime Dénès | |
| 2017-11-16 | Merge PR #6023: Use GHC.Base.Any for compatibility with GHC 8.2 | Maxime Dénès | |
| 2017-11-16 | Fix micromega.ml to match generated file and enforce match in make. | Gaëtan Gilbert | |
| Mismatch probably caused by c5aca4005. | |||
| 2017-11-15 | Fixing printing of tactics encapsulated as tacarg with Tacexp. | Hugo Herbelin | |
| We preserve the level instead of resetting it at level 0. Probably it would be the same as giving level ltop since Tacexp apparently comes only from using a tactic in an Ltac "let", which is where I observed a problem. | |||
| 2017-11-15 | Using "l" printer for glob_constr, like for constr. | Hugo Herbelin | |
| This is to avoid excessive parentheses, in particular when printing "constr:()" in "Print Ltac f". | |||
| 2017-11-13 | [api] Another large deprecation, `Nameops` | Emilio Jesus Gallego Arias | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |