| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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-12-01 | Documenting the -Q flag of coqchk. | Pierre-Marie Pédrot | |
| 2017-12-01 | Merge PR #736: [ci] Test coqchk on the CompCert target. | Maxime Dénès | |
| 2017-12-01 | Merge PR #6256: CI: better ocaml warning checks | Maxime Dénès | |
| 2017-12-01 | Merge PR #6276: Coqchk accepts filenames | Maxime Dénès | |
| 2017-12-01 | Merge PR #6233: [proof] [api] Rename proof types in preparation for ↵ | Maxime Dénès | |
| functionalization. | |||
| 2017-11-30 | Merge PR #1049: Remove obsolete locality | Maxime Dénès | |
| 2017-11-30 | Merge PR #6244: [lib] [api] Introduce record for `object_prefix` | Maxime Dénès | |
| 2017-11-30 | [ci] Test coqchk on the CompCert target. | Théo Zimmermann | |
| 2017-11-30 | Merge PR #6274: Attempt to fix inversion disregarding singleton types (fixes ↵ | Maxime Dénès | |
| #3125) | |||
| 2017-11-30 | Remove unused boolean from cl_context field of Typeclasses.typeclass | Gaëtan Gilbert | |
| 2017-11-30 | Add merlin in the dependencies of nix-shell only. | Théo Zimmermann | |
| 2017-11-30 | Merge PR #6269: [ci] [vst] Shorten compilation time to avoid Travis timeouts. | Maxime Dénès | |
| 2017-11-30 | Merge PR #6193: Fix (partial) #4878: option to stop autodeclaring axiom as ↵ | Maxime Dénès | |
| instance. | |||
| 2017-11-30 | Warning for absolute name masking (making it deprecated, should become | Matthieu Sozeau | |
| an error) | |||
| 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-29 | Fix usage comment. | Théo Zimmermann | |
| 2017-11-29 | This script apparently uses bash-specific features. | Théo Zimmermann | |
| 2017-11-29 | Fix PR merge script. | Théo Zimmermann | |
| Was still relying on the existence of user-configured /pr/. | |||
| 2017-11-29 | [lib] [api] Introduce record for `object_prefix` | Emilio Jesus Gallego Arias | |
| This is a minor cleanup adding a record in a try to structure the state living in `Lib`. | |||
| 2017-11-29 | Forbid implicitly relative names in the checker. | Pierre-Marie Pédrot | |
| Before this patch, passing a mere identifier (without dots) to the checker would make it consider it as implicitly referring to a relative name. For instance, if passed "foo", it would have looked for "Bar.foo.vo" and "Qux.foo.vo" if those files were in the loadpath. This was quite ad-hoc. We remove this "feature" and require the user to always give either a filename or a fully qualified logical name. | |||
| 2017-11-29 | Mark the -I option in coqchk as deprecated and merge it with -Q. | Pierre-Marie Pédrot | |
| It is not doing the same thing as coqtop, and the corresponding coqtop semantics is irrelevant in the checker as the latter does not rely on ML code. | |||
| 2017-11-29 | Add a -Q option to coqchck. | Pierre-Marie Pédrot | |
| It has exactly the same effect as -R, because there is no such thing as implicit relativization for object files in coqchk, contrarily to what Require does in coqtop. | |||
| 2017-11-29 | [proof] [api] Rename proof types in preparation for functionalization. | Emilio Jesus Gallego Arias | |
| In particular `Proof_global.t` will become a first class object for the upper parts of the system in a next commit. | |||
| 2017-11-29 | Merge PR #6271: Add PR backport script. | Maxime Dénès | |
| 2017-11-29 | Merge PR #6253: Fixing inconsistent associativity of level 10 in the table ↵ | Maxime Dénès | |
| of levels | |||
| 2017-11-29 | Merge PR #6199: [vernac] Uniformize type of vernac interpretation. | Maxime Dénès | |
| 2017-11-29 | coq_makefile: pass filenames to coqchk | Ralf Jung | |
| 2017-11-29 | Documenting the possibility to pass filenames to coqchk. | Pierre-Marie Pédrot | |
| 2017-11-29 | Allow to pass physical files to coqchk. | Pierre-Marie Pédrot | |
| 2017-11-28 | In injection/inversion, consider all template-polymorphic types as injectable. | Hugo Herbelin | |
| In particular singleton inductive types are considered injectable, even in the absence of the option "Set Keep Proof Equalities". This fixes #3125 (and #4560, #6273). | |||
| 2017-11-28 | use \ocaml macro in new text | Paul Steckler | |
| 2017-11-28 | Adding a variant get_truncation_family_of of get_sort_family_of. | Hugo Herbelin | |
| This function returns InProp or InSet for inductive types only when the inductive type has been explicitly truncated to Prop or (impredicative) Set. For instance, singleton inductive types and small (predicative) inductive types are not truncated and hence in Type. | |||
| 2017-11-28 | Moving non-recursive function sort_family_of out of the retype block of ↵ | Hugo Herbelin | |
| recursive functions. | |||
| 2017-11-28 | Adding an interface file for checker/check.ml. | Pierre-Marie Pédrot | |
| 2017-11-28 | more complete not-fully-applied error messages, #6145 | Paul Steckler | |
| 2017-11-28 | Add PR backport script. | Théo Zimmermann | |
| 2017-11-28 | [toplevel] Properly redirect stdout on `Redirect` vernac. | Emilio Jesus Gallego Arias | |
| Fixes #6130, it was a silly omission from a previous output refactoring. We redirect all channels as this was the implied semantics of the old command. | |||
| 2017-11-28 | [ci] [vst] Shorten compilation time to avoid Travis timeouts. | Emilio Jesus Gallego Arias | |
| We remove the progs target [examples] to save time, we still build the full library thou. I guess we can't do better for now unless we get some Travis subscription. | |||
| 2017-11-28 | Use safe demarshalling in the checker. | Pierre-Marie Pédrot | |
| Instead of relying on the OCaml demarshaller, which is not resilient against ill-formed data, we reuse the safe demarshaller from votour. This ensures that garbage files do not trigger memory violations. | |||
| 2017-11-28 | Use large arrays in the checker demarshaller. | Pierre-Marie Pédrot | |
| This allows to work around the size limitation of vanilla OCaml arrays on 32-bit platforms, which is rather easy to hit. | |||
| 2017-11-28 | CI: use -byte-only in [warnings] jobs. | Gaëtan Gilbert | |
| This avoids mixing native and byte compilation as the debug printers are always byte compiled and the tools have no .byte rule, only the OCAMLBEST rule. | |||
| 2017-11-28 | Fix native compute for byte compiled Coq. | Gaëtan Gilbert | |
| 2017-11-28 | Fix (partial) #4878: option to stop autodeclaring axiom as instance. | Gaëtan Gilbert | |
| 2017-11-28 | Make the micromega extraction check a regular output test. | Gaëtan Gilbert | |
| This allows us to enforce that it works without breaking the build when it doesn't. | |||
| 2017-11-28 | Travis: do not build stdlib in [warnings] jobs. | Gaëtan Gilbert | |
| 2017-11-28 | Add alienclean target to remove compilation products with no source. | Gaëtan Gilbert | |
| 2017-11-28 | Merge PR #6259: Add PR merge script. | Maxime Dénès | |
| 2017-11-28 | Add PR merge script. | Maxime Dénès | |
| 2017-11-28 | Merge PR #1033: Universe binder improvements | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |