| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-04-06 | Merge PR#455: Farewell decl_mode | Maxime Dénès | |
| 2017-04-06 | Merge PR#488: Adding a documentation for the new proof engine. | Maxime Dénès | |
| 2017-04-06 | Adding a documentation for the new proof engine. | Pierre-Marie Pédrot | |
| 2017-04-06 | Merge PR#508: Optimize pending evars | Maxime Dénès | |
| 2017-04-06 | Merge PR#542: [travis] Add webhook to Gitter. | Maxime Dénès | |
| 2017-04-06 | [travis] Add webhook to Gitter. | Théo Zimmermann | |
| 2017-04-05 | Merge PR#434: Optimizing array mapping in the kernel. | Maxime Dénès | |
| 2017-04-04 | Merge PR#502: [pp] Add anomaly header to error messages. | Maxime Dénès | |
| 2017-04-03 | Merge branch 'v8.6' into trunk | Maxime Dénès | |
| 2017-04-03 | Merge PR#533: Instances should obey universe binders even when defined by ↵ | Maxime Dénès | |
| tactics. | |||
| 2017-04-03 | Fix loading of ocamldebug printers. | Pierre-Marie Pédrot | |
| 2017-04-03 | Instances should obey universe binders even when defined by tactics. | Gaetan Gilbert | |
| 2017-04-03 | Merge PR#417: No cast surgery in let in | Maxime Dénès | |
| 2017-04-03 | Add test file for #4957. | Maxime Dénès | |
| Bug #4957 was "unify cannot directly unify universes with evars, but can do so indirectly". | |||
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |