Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
| * | | | | | | | | | | | | | | | Merge PR#521: Do so that "About" tells if a reference is a coercion. | 2017-03-29 | ||
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR#525: [ide] Fix typo in pp serialization. | 2017-03-29 | ||
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | |_|_|_|_|_|_|_|_|_|_|_|/ / / / | |/| | | | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | | | | Merge branch 'trunk' into pr379 | 2017-03-29 | ||
|\| | | | | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | | | | Fix call to broken unsafe_type_of in apply tactic. | 2017-03-29 | ||
| | | | | | | | | | * | | | | | | | Run non-tactic comands without resilient_command | 2017-03-29 | ||
| | | | | | |_|_|_|/ / / / / / / | | | | | |/| | | | | | | | | | | ||||
| | * | | | | | | | | | | | | | | [ide] Fix typo in pp serialization. | 2017-03-29 | ||
* | | | | | | | | | | | | | | | | Revert to incorrect heuristic in apply. | 2017-03-28 | ||
| * | | | | | | | | | | | | | | | Fixing missing PropFacts.v in Logic/vo.itarget. | 2017-03-28 | ||
| |/ / / / / / / / / / / / / / | ||||
| | | | | | * / / / / / / / / | [coqide] Protect against size_allocate race in proofview. | 2017-03-28 | ||
| | |_|_|_|/ / / / / / / / / | |/| | | | | | | | | | | | | ||||
| | * | | | | | | | | | | | | Do so that "About" tells if a reference is a coercion. | 2017-03-27 | ||
| |/ / / / / / / / / / / / | ||||
| | | | | | | | | | | | * | More efficient check in validity of side-effects. | 2017-03-27 | ||
| | | | | | | | | | | | * | Adding the size of the opaquetab in its representation. | 2017-03-27 | ||
| | | | | | | | | | | | * | Fix hashconsing of terms in the kernel. | 2017-03-27 | ||
| | |_|_|_|_|_|_|_|_|_|/ | |/| | | | | | | | | | | ||||
* | | | | | | | | | | | | Mathcomp overlay. | 2017-03-25 | ||
* | | | | | | | | | | | | Fix interpretation of Ltac patterns episode 2. | 2017-03-24 | ||
* | | | | | | | | | | | | Merge branch 'trunk' into pr379 | 2017-03-24 | ||
|\| | | | | | | | | | | | ||||
| | | | * | | | | | | | | [travis] Backport from trunk: VST | 2017-03-24 | ||
| | | |/ / / / / / / / | ||||
| * | | | | | | | | | | Merge PR#489: [travis] Add VST | 2017-03-24 | ||
| |\ \ \ \ \ \ \ \ \ \ | ||||
| | | | | * | | | | | | | [stm] Remove some obsolete vernacs/classification. | 2017-03-24 | ||
| | | * | | | | | | | | | [nit] Fix a couple incorrect uses of msg_error. | 2017-03-24 | ||
| | | | |/ / / / / / / | | | |/| | | | | | | | ||||
| | * / | | | | | | | | [travis] Add VST | 2017-03-24 | ||
| | |/ / / / / / / / | ||||
| | | | | * | | | | | Applying same convention as in Definition for printing type in a let in. | 2017-03-24 | ||
| | | | | * | | | | | Applying same convention as in Definition for parsing type in a let in. | 2017-03-24 | ||
| | | | | * | | | | | Documenting main changes of API. | 2017-03-24 | ||
| | | | | * | | | | | Replacing "cast surgery" in LetIn by a proper field (see PR #404). | 2017-03-24 | ||
| | | | | * | | | | | Using the same type of binders for interning and externing. | 2017-03-24 | ||
| | | | | * | | | | | Unifying standard "constr_level" names for constructors of local_binder_expr. | 2017-03-24 | ||
| | | | | * | | | | | Renaming local_binder into local_binder_expr. | 2017-03-24 | ||
| | | | | * | | | | | Merging glob_binder and glob_decl. | 2017-03-24 | ||
| | | | | * | | | | | Type extended_glob_local_binder now contains only glob_constr. | 2017-03-24 | ||
| | | | | * | | | | | Standardized the order of constructors for binders: Assum then Def. | 2017-03-24 | ||
| | | | | * | | | | | Cleaning phase around local binder at glob level: | 2017-03-24 | ||
| | | | | * | | | | | "Standardizing" the name LocalPatten into LocalRawPattern. | 2017-03-24 | ||
| | |_|_|/ / / / / | |/| | | | | | | | ||||
| | | | | | | * | | Better algorithm for Evarconv.max_undefined_with_candidates. | 2017-03-24 | ||
| * | | | | | | | | Merge PR#392: strengthened the statement of JMeq_eq_dep | 2017-03-24 | ||
| |\ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ | Merge branch 'v8.6' into trunk | 2017-03-24 | ||
| |\ \ \ \ \ \ \ \ \ | | | |_|/ / / / / / | | |/| | | | | | | | ||||
| | * | | | | | | | | Merge PR#476: [future] Be eager when "chaining" already resolved future values. | 2017-03-24 | ||
| | |\ \ \ \ \ \ \ \ | ||||
| | * \ \ \ \ \ \ \ \ | Merge PR#475: Opaque side effects | 2017-03-24 | ||
| | |\ \ \ \ \ \ \ \ \ | ||||
| * | \ \ \ \ \ \ \ \ \ | Merge PR#504: [META] add support for ide libraries | 2017-03-24 | ||
| |\ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ | Merge PR#503: make check not CoqIDE-specific | 2017-03-23 | ||
| |\ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR#433: doc: fix a French-ism | 2017-03-23 | ||
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | | |_|_|_|_|_|_|/ / / / / / | |/| | | | | | | | | | | | | ||||
| * | | | | | | | | | | | | | Merge branch 'v8.6' into trunk | 2017-03-23 | ||
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | | | |_|_|/ / / / / / / / / | | |/| | | | | | | | | | | | ||||
| | * | | | | | | | | | | | | Merge PR#507: Intern names bound in match patterns | 2017-03-23 | ||
| | |\ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | * | | | | | | | | Documenting the API of side-effects. | 2017-03-23 | ||
| | | | | | | * | | | | | | | | Using a dedicated datastructure for side effect ordering. | 2017-03-23 | ||
| | | | | | | * | | | | | | | | Making the side_effects type opaque. | 2017-03-23 | ||
| | | |_|_|_|/ / / / / / / / | | |/| | | | | | | | | | | | ||||
| | | * | | | | | | | | | | | Intern names bound in match patterns | 2017-03-23 | ||
| * | | | | | | | | | | | | | Merge PR#501: [travis] Fix iris-coq build. | 2017-03-23 | ||
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge branch 'v8.6' into trunk | 2017-03-23 | ||
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | |/ / / / / / / / / / / / | | |/| | | | | | | | | | | | | ||||
| | * | | | | | | | | | | | | | Merge PR#497: [travis] [8.6.only] Backport latest changes from trunk. | 2017-03-23 | ||
| | |\ \ \ \ \ \ \ \ \ \ \ \ \ |