| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-12-05 | Merge PR #6210: More complete not-fully-applied error messages, #6145 | Maxime Dénès | |
| 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 | 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-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 | [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 | [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 | 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 | [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 | 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 | Travis: do not build stdlib in [warnings] jobs. | 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 | |
| 2017-11-28 | Merge PR #6235: Fixing failing mkdir in test-suite for coq-makefile. | Maxime Dénès | |
| 2017-11-28 | Merge PR #6248: [api] Remove aliases of `Evar.t` | Maxime Dénès | |
| 2017-11-28 | Merge PR #6246: Ref. Man.: Updating the current official writing of OCaml; ↵ | Maxime Dénès | |
| updating Camlp4->Camlp5. | |||
| 2017-11-27 | [vernac] Adjust `interp` to pass polymorphic in the attributes. | Emilio Jesus Gallego Arias | |
| 2017-11-27 | [vernac] Add polymorphic to the type of vernac interpration options. | Emilio Jesus Gallego Arias | |
| 2017-11-27 | [vernac] Start to uniformize type of vernac interpretation. | Emilio Jesus Gallego Arias | |
| In particular, we put all the context in the atts structure, and generalize the type of the parameters of a vernac. I hope this helps people working on "attributes", my motivation is indeed having a more robust interpretation. | |||
| 2017-11-27 | Merge PR #6237: coq_makefile tests: build in easily removed temporary ↵ | Maxime Dénès | |
| subdirectory. | |||
| 2017-11-27 | Merge PR #6242: Use Evarutil.has_undefined_evars for tactic has_evar. | Maxime Dénès | |
| 2017-11-27 | Merge PR #6236: Fix coq-makefile ocamldoc call when configured with -annotate. | Maxime Dénès | |
| 2017-11-27 | Merge PR #6207: [stm] Allow delayed constant in interactive mode. | Maxime Dénès | |
| 2017-11-27 | Merge PR #6238: Fix deprecated syntax warning from vernacextend.mlp. | Maxime Dénès | |
| 2017-11-27 | Merge PR #6241: [lib] Generalize Control.timeout type. | Maxime Dénès | |
| 2017-11-27 | Merge PR #6228: Make byte on gitlab. | Maxime Dénès | |
| 2017-11-27 | Merge PR #6226: Enhance votour | Maxime Dénès | |
| 2017-11-27 | Merge PR #6149: Update TimeFileMaker.py to correctly sort timing diffs | Maxime Dénès | |
| 2017-11-27 | Merge PR #6041: Protecting the printing of filenames with space | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |