aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Merge PR#417: No cast surgery in let inGravatar Maxime Dénès2017-04-03
|\
* | Fix higher-order pattern variables not being printed as "@?" (bug #5431).Gravatar Guillaume Melquiond2017-04-02
| |
* | Fix documentation typo (bug #5433).Gravatar Guillaume Melquiond2017-04-02
| |
* | Simplify some proofs.Gravatar Guillaume Melquiond2017-04-02
| | | | | | | | | | | | | | | | 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.
* | Declaring ltac plugin, so that static linking works.Gravatar Hugo Herbelin2017-04-01
| |
* | Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-03-30
|\ \
| * \ Merge PR#463: Run non-tactic comands without resilient_commandGravatar Maxime Dénès2017-03-30
| |\ \
* | | | Fix ring_simplify sometimes producing R0 and R1 instead of 0%R and 1%R.Gravatar Guillaume Melquiond2017-03-30
| | | |
* | | | Merge PR#469: Added take to VectorDefGravatar Maxime Dénès2017-03-30
|\ \ \ \
| * | | | Added take to VectorDef.Gravatar George Stelle2017-03-30
| | | | | | | | | | | | | | | | | | | | | | | | | Added a function that takes the first [p] elements of a vector, and a few lemmas proving some of its properties.
* | | | | Merge PR#511: [stm] Remove some obsolete vernacs/classification.Gravatar Maxime Dénès2017-03-30
|\ \ \ \ \
* \ \ \ \ \ Merge PR#522: [coqide] Protect against size_allocate race in proofview.Gravatar Maxime Dénès2017-03-29
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-03-29
|\ \ \ \ \ \ \ | | |_|_|/ / / | |/| | | | |
| * | | | | | Merge PR#514: [travis] Backport from trunk: VSTGravatar Maxime Dénès2017-03-29
| |\ \ \ \ \ \
* | \ \ \ \ \ \ Merge PR#506: [nit] Fix a couple incorrect uses of msg_error.Gravatar Maxime Dénès2017-03-29
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR#521: Do so that "About" tells if a reference is a coercion.Gravatar Maxime Dénès2017-03-29
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR#525: [ide] Fix typo in pp serialization.Gravatar Maxime Dénès2017-03-29
|\ \ \ \ \ \ \ \ \ \
| | | | | | | | | * | Run non-tactic comands without resilient_commandGravatar Tej Chajed2017-03-29
| | | | | |_|_|_|/ / | | | | |/| | | | |
| * | | | | | | | | [ide] Fix typo in pp serialization.Gravatar Emilio Jesus Gallego Arias2017-03-29
| | | | | | | | | |
* | | | | | | | | | Fixing missing PropFacts.v in Logic/vo.itarget.Gravatar Hugo Herbelin2017-03-28
|/ / / / / / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | | | * / / / [coqide] Protect against size_allocate race in proofview.Gravatar Emilio Jesus Gallego Arias2017-03-28
| |_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
| * | | | | | | Do so that "About" tells if a reference is a coercion.Gravatar Hugo Herbelin2017-03-27
|/ / / / / / /
| | | * / / / [travis] Backport from trunk: VSTGravatar Emilio Jesus Gallego Arias2017-03-24
| | |/ / / /
* | | | | | Merge PR#489: [travis] Add VSTGravatar Maxime Dénès2017-03-24
|\ \ \ \ \ \
| | | | * | | [stm] Remove some obsolete vernacs/classification.Gravatar Emilio Jesus Gallego Arias2017-03-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | * | | | | [nit] Fix a couple incorrect uses of msg_error.Gravatar Emilio Jesus Gallego Arias2017-03-24
| | | |/ / / | | |/| | |
| * / | | | [travis] Add VSTGravatar Emilio Jesus Gallego Arias2017-03-24
| |/ / / /
| | | | * Applying same convention as in Definition for printing type in a let in.Gravatar Hugo Herbelin2017-03-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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 *)
| | | | * Applying same convention as in Definition for parsing type in a let in.Gravatar Hugo Herbelin2017-03-24
| | | | |
| | | | * Documenting main changes of API.Gravatar Hugo Herbelin2017-03-24
| | | | |
| | | | * Replacing "cast surgery" in LetIn by a proper field (see PR #404).Gravatar Hugo Herbelin2017-03-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | | * Using the same type of binders for interning and externing.Gravatar Hugo Herbelin2017-03-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Previously a union type was used for externing. In particular, moving extended_glob_local_binder to glob_constr.ml.
| | | | * Unifying standard "constr_level" names for constructors of local_binder_expr.Gravatar Hugo Herbelin2017-03-24
| | | | | | | | | | | | | | | | | | | | RawLocal -> CLocal
| | | | * Renaming local_binder into local_binder_expr.Gravatar Hugo Herbelin2017-03-24
| | | | | | | | | | | | | | | | | | | | This is a bit long, but it is to keep a symmetry with constr_expr.
| | | | * Merging glob_binder and glob_decl.Gravatar Hugo Herbelin2017-03-24
| | | | |
| | | | * Type extended_glob_local_binder now contains only glob_constr.Gravatar Hugo Herbelin2017-03-24
| | | | | | | | | | | | | | | | | | | | No more constr_expr in it.
| | | | * Standardized the order of constructors for binders: Assum then Def.Gravatar Hugo Herbelin2017-03-24
| | | | |
| | | | * Cleaning phase around local binder at glob level:Gravatar Hugo Herbelin2017-03-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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).
| | | | * "Standardizing" the name LocalPatten into LocalRawPattern.Gravatar Hugo Herbelin2017-03-24
| |_|_|/ |/| | |
* | | | Merge PR#392: strengthened the statement of JMeq_eq_depGravatar Maxime Dénès2017-03-24
|\ \ \ \
* \ \ \ \ Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-03-24
|\ \ \ \ \ | | |_|/ / | |/| | |
| * | | | Merge PR#476: [future] Be eager when "chaining" already resolved future values.Gravatar Maxime Dénès2017-03-24
| |\ \ \ \
| * \ \ \ \ Merge PR#475: Opaque side effectsGravatar Maxime Dénès2017-03-24
| |\ \ \ \ \
* | \ \ \ \ \ Merge PR#504: [META] add support for ide librariesGravatar Maxime Dénès2017-03-24
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR#503: make check not CoqIDE-specificGravatar Maxime Dénès2017-03-23
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR#433: doc: fix a French-ismGravatar Maxime Dénès2017-03-23
|\ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|/ / |/| | | | | | | |
* | | | | | | | | Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-03-23
|\ \ \ \ \ \ \ \ \ | | |_|_|/ / / / / | |/| | | | | | |
| * | | | | | | | Merge PR#507: Intern names bound in match patternsGravatar Maxime Dénès2017-03-23
| |\ \ \ \ \ \ \ \
| | | | | | * | | | Documenting the API of side-effects.Gravatar Pierre-Marie Pédrot2017-03-23
| | | | | | | | | |
| | | | | | * | | | Using a dedicated datastructure for side effect ordering.Gravatar Pierre-Marie Pédrot2017-03-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 05:22:04 +0000