| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-04-03 | Merge PR#417: No cast surgery in let in | Maxime Dénès | |
| 2017-04-02 | Fix higher-order pattern variables not being printed as "@?" (bug #5431). | Guillaume Melquiond | |
| 2017-04-02 | Fix documentation typo (bug #5433). | Guillaume Melquiond | |
| 2017-04-02 | Simplify some proofs. | Guillaume Melquiond | |
| This commit does not modify the signature of the involved modules, only the opaque proof terms. One has to wonder how proofs can bitrot so much that several occurrences of "replace 4 with 4" start appearing. | |||
| 2017-04-01 | Declaring ltac plugin, so that static linking works. | Hugo Herbelin | |
| 2017-03-30 | Merge branch 'v8.6' into trunk | Maxime Dénès | |
| 2017-03-30 | Merge PR#463: Run non-tactic comands without resilient_command | Maxime Dénès | |
| 2017-03-30 | Fix ring_simplify sometimes producing R0 and R1 instead of 0%R and 1%R. | Guillaume Melquiond | |
| 2017-03-30 | Merge PR#469: Added take to VectorDef | Maxime Dénès | |
| 2017-03-30 | Added take to VectorDef. | George Stelle | |
| Added a function that takes the first [p] elements of a vector, and a few lemmas proving some of its properties. | |||
| 2017-03-30 | Merge PR#511: [stm] Remove some obsolete vernacs/classification. | Maxime Dénès | |
| 2017-03-29 | Merge PR#522: [coqide] Protect against size_allocate race in proofview. | Maxime Dénès | |
| 2017-03-29 | Merge branch 'v8.6' into trunk | Maxime Dénès | |
| 2017-03-29 | Merge PR#514: [travis] Backport from trunk: VST | Maxime Dénès | |
| 2017-03-29 | Merge PR#506: [nit] Fix a couple incorrect uses of msg_error. | Maxime Dénès | |
| 2017-03-29 | Merge PR#521: Do so that "About" tells if a reference is a coercion. | Maxime Dénès | |
| 2017-03-29 | Merge PR#525: [ide] Fix typo in pp serialization. | Maxime Dénès | |
| 2017-03-29 | Run non-tactic comands without resilient_command | Tej Chajed | |
| 2017-03-29 | [ide] Fix typo in pp serialization. | Emilio Jesus Gallego Arias | |
| 2017-03-28 | Fixing missing PropFacts.v in Logic/vo.itarget. | Hugo Herbelin | |
| This is while waiting for a possible different solution, if ever such a different solution is adopted, since the coq.inria.fr/library has currently a broken link and someone rightly complained about it. | |||
| 2017-03-28 | [coqide] Protect against size_allocate race in proofview. | Emilio Jesus Gallego Arias | |
| To handle dynamic printing in CoqIDE we listen to the `size_allocate` signal , [see more details in 6885a398229918865378ea24f07d93d2bcdd2802] However, we must be careful to protect against scrollbar creation: it is possible for the `size_allocate` handler to change the size when inserting text (due to scrollbars), thus we may enter in an infinite loop. Our fix is to check if the width has really changed, as done in `Wg_MessageView`. This fixes the problem noted by @herbelin in https://coq.inria.fr/bugs/show_bug.cgi?id=5417 | |||
| 2017-03-27 | Do so that "About" tells if a reference is a coercion. | Hugo Herbelin | |
| 2017-03-24 | [travis] Backport from trunk: VST | Emilio Jesus Gallego Arias | |
| 2017-03-24 | Merge PR#489: [travis] Add VST | Maxime Dénès | |
| 2017-03-24 | [stm] Remove some obsolete vernacs/classification. | Emilio Jesus Gallego Arias | |
| This is the good parts of PR #360. IIUC, these vernacular were meant mostly for debugging and they are not supposed to be of any use these days. Back and join are still there not to break the testing infrastructure, but some day they should go away. | |||
| 2017-03-24 | [nit] Fix a couple incorrect uses of msg_error. | Emilio Jesus Gallego Arias | |
| 2017-03-24 | [travis] Add VST | Emilio Jesus Gallego Arias | |
| 2017-03-24 | Applying same convention as in Definition for printing type in a let in. | Hugo Herbelin | |
| Also adding spaces around ":=" and ":" when printed as "(x : t := c)". Example: Check fun y => let x : True := I in fun z => z+y=0. (* λ (y : nat) (x : True := I) (z : nat), z + y = 0 : nat → nat → Prop *) | |||
| 2017-03-24 | Applying same convention as in Definition for parsing type in a let in. | Hugo Herbelin | |
| 2017-03-24 | Documenting main changes of API. | Hugo Herbelin | |
| 2017-03-24 | Replacing "cast surgery" in LetIn by a proper field (see PR #404). | Hugo Herbelin | |
| This is a patch fulfilling the relevant remark of Maxime that an explicit information at the ML type level would be better than "cast surgery" to carry the optional type of a let-in. There are a very few semantic changes. - a "(x:t:=c)" in a block of binders is now written in the more standard way "(x:=c:t)" - in notations, the type of a let-in is not displayed if not explicitly asked so. See discussion at PR #417 for more information. | |||
| 2017-03-24 | Using the same type of binders for interning and externing. | Hugo Herbelin | |
| Previously a union type was used for externing. In particular, moving extended_glob_local_binder to glob_constr.ml. | |||
| 2017-03-24 | Unifying standard "constr_level" names for constructors of local_binder_expr. | Hugo Herbelin | |
| RawLocal -> CLocal | |||
| 2017-03-24 | Renaming local_binder into local_binder_expr. | Hugo Herbelin | |
| This is a bit long, but it is to keep a symmetry with constr_expr. | |||
| 2017-03-24 | Merging glob_binder and glob_decl. | Hugo Herbelin | |
| 2017-03-24 | Type extended_glob_local_binder now contains only glob_constr. | Hugo Herbelin | |
| No more constr_expr in it. | |||
| 2017-03-24 | Standardized the order of constructors for binders: Assum then Def. | Hugo Herbelin | |
| 2017-03-24 | Cleaning phase around local binder at glob level: | Hugo Herbelin | |
| Aligned the type binder_data to the naming scheme used in (raw) local_binder and Rel.Declaration.t. Made some code factorization. Still to do: align type Glob_term.glob_binder to the Assum/Def format too. Note: this includes fix of anomaly with 'pat in cofix (dec77f282). | |||
| 2017-03-24 | "Standardizing" the name LocalPatten into LocalRawPattern. | Hugo Herbelin | |
| 2017-03-24 | Merge PR#392: strengthened the statement of JMeq_eq_dep | Maxime Dénès | |
| 2017-03-24 | Merge branch 'v8.6' into trunk | Maxime Dénès | |
| 2017-03-24 | Merge PR#476: [future] Be eager when "chaining" already resolved future values. | Maxime Dénès | |
| 2017-03-24 | Merge PR#475: Opaque side effects | Maxime Dénès | |
| 2017-03-24 | Merge PR#504: [META] add support for ide libraries | Maxime Dénès | |
| 2017-03-23 | Merge PR#503: make check not CoqIDE-specific | Maxime Dénès | |
| 2017-03-23 | Merge PR#433: doc: fix a French-ism | Maxime Dénès | |
| 2017-03-23 | Merge branch 'v8.6' into trunk | Maxime Dénès | |
| 2017-03-23 | Merge PR#507: Intern names bound in match patterns | Maxime Dénès | |
| 2017-03-23 | Documenting the API of side-effects. | Pierre-Marie Pédrot | |
| 2017-03-23 | Using a dedicated datastructure for side effect ordering. | Pierre-Marie Pédrot | |
| We were doing fishy things in the Term_typing file, where side-effects were not considered in the right uniquization order because of the uniq_seff_rev function. It probably did not matter after a9b76df because effects were (mostly) uniquize upfront, but this is not clear because of the use of the transparente API in the module. Now everything has to go through the opaque API, so that a proper dependence order is ensured. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |