Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
| | * | | | | Drop '.' from CErrors.anomaly, insert it in args | 2017-06-02 | ||
| | * | | | | Don't double up on periods in anomalies | 2017-06-02 | ||
| |/ / / / |/| | | | | ||||
* | | | | | Merge PR#670: Postponing of universe constraints unification in term equality. | 2017-06-01 | ||
|\ \ \ \ \ | ||||
* \ \ \ \ \ | Merge PR#696: Trunk+cleanup constr of global | 2017-06-01 | ||
|\ \ \ \ \ \ | ||||
* \ \ \ \ \ \ | Merge PR#561: Improving the Name API | 2017-06-01 | ||
|\ \ \ \ \ \ \ | ||||
| | | | | | | * | Bump year in headers. | 2017-06-01 | ||
* | | | | | | | | Merge PR#694: Fixing #5523 (missing support for complex constructions in recu... | 2017-06-01 | ||
|\ \ \ \ \ \ \ \ | ||||
| | | | | | * \ \ | Merge PR#560: Reinstate fixpoint refolding in [cbn], deactivated by mistake (... | 2017-05-31 | ||
| | | | | | |\ \ \ | | | | | | | |_|/ | | | | | | |/| | | ||||
| | | | | * | | | | Using a more explicit algebraic type for evars of kind "MatchingVar". | 2017-05-31 | ||
| | * | | | | | | | Creating a module Nameops.Name extending module Names.Name. | 2017-05-31 | ||
| | | |_|/ / / / | | |/| | | | | | ||||
| * / | | | | | | Fixing #5523 (missing support for complex constructions in recursive notations). | 2017-05-31 | ||
| |/ / / / / / | ||||
* / / / / / / | Support for using type information to infer more precise evar sources. | 2017-05-30 | ||
|/ / / / / / | ||||
| * / / / / | Pretyping cleanup: remove constr_of_global calls | 2017-05-29 | ||
|/ / / / / | ||||
| | * | | | Merge PR#546: Fix for bug #4499 and other minor related bugs | 2017-05-29 | ||
| | |\ \ \ | ||||
* | | \ \ \ | Merge PR#512: [cleanup] Unify all calls to the error function. | 2017-05-29 | ||
|\ \ \ \ \ \ | ||||
| * | | | | | | [cleanup] Unify all calls to the error function. | 2017-05-27 | ||
* | | | | | | | [coqlib] Move `Coqlib` to `library/`. | 2017-05-27 | ||
|/ / / / / / | ||||
* | | | | | | Merge PR#608: Allow Ltac2 as a plugin | 2017-05-25 | ||
|\ \ \ \ \ \ | ||||
* \ \ \ \ \ \ | Merge PR#481: [option] Remove support for non-synchronous options. | 2017-05-25 | ||
|\ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ | Merge branch 'trunk' into located_switch | 2017-05-24 | ||
|\ \ \ \ \ \ \ \ | ||||
| | * | | | | | | | [option] Remove support for non-synchronous options. | 2017-05-24 | ||
| * | | | | | | | | Merge PR#650: Fixing an extra bug with pattern_of_constr | 2017-05-24 | ||
| |\ \ \ \ \ \ \ \ | ||||
| * | | | | | | | | | unification.mli: Fix a spelling typo in a comment | 2017-05-23 | ||
| | |/ / / / / / / | |/| | | | | | | | ||||
| | | | * | | | | | Postponing of universe constraints unification in term equality. | 2017-05-23 | ||
| | |_|/ / / / / | |/| | | | | | | ||||
| | * | | | | | | Fixing an extra bug with pattern_of_constr. | 2017-05-19 | ||
| |/ / / / / / | ||||
| | * | | | | | Merge branch 'master' into ltac2-hooks | 2017-05-19 | ||
| | |\ \ \ \ \ | | |/ / / / / | |/| | | | | | ||||
| | | * | | | | fix swapping of ids in tuples, bug 5486 | 2017-05-17 | ||
| * | | | | | | Merge branch 'v8.6' | 2017-05-17 | ||
| |\ \ \ \ \ \ | | | |/ / / / | | |/| | | | | ||||
| | * | | | | | Removing a line warned unused. | 2017-05-14 | ||
| * | | | | | | Merge PR#594: An example showing the benefit of Econstr | 2017-05-11 | ||
| |\ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ | Merge PR#373: A refined solution to the beta-iota discrepancies between 8.4 a... | 2017-05-11 | ||
| |\ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ | Merge PR#606: Added an option Set Debug Cbv | 2017-05-09 | ||
| |\ \ \ \ \ \ \ \ | ||||
| * | | | | | | | | | Remove dead code and unused open. | 2017-05-05 | ||
| * | | | | | | | | | Merge PR#558: Adding a fold_glob_constr_with_binders combinator | 2017-05-05 | ||
| |\ \ \ \ \ \ \ \ \ | ||||
| | | | | * | | | | | | Upgrading some local function as a general-purpose combinator Option.List.map. | 2017-05-05 | ||
| | |_|_|/ / / / / / | |/| | | | | | | | | ||||
| * | | | | | | | | | Merge PR#544: Anonymous universes | 2017-05-05 | ||
| |\ \ \ \ \ \ \ \ \ | ||||
| | | | | | | * | | | | Generalizing the tactic-in-term embedding to any generic argument. | 2017-05-03 | ||
| | |_|_|_|_|/ / / / | |/| | | | | | | | | ||||
| * | | | | | | | | | Merge PR#404: patch for printing types of let bindings | 2017-05-03 | ||
| |\ \ \ \ \ \ \ \ \ | ||||
| | | | | * | | | | | | Added an option Set Debug Cbv. | 2017-05-03 | ||
| | |_|_|/ / / / / / | |/| | | | | | | | | ||||
| | | * | | | | | | | Type@{_} should not produce a flexible algebraic universe. | 2017-05-03 | ||
| | | * | | | | | | | Allow flexible anonymous universes in instances and sorts. | 2017-05-03 | ||
| * | | | | | | | | | Merge PR#411: Mention template polymorphism in the documentation. | 2017-05-03 | ||
| |\ \ \ \ \ \ \ \ \ | | |_|/ / / / / / / | |/| | | | | | | | | ||||
| | | * | | | | | | | applied the patch for printing types of let bindings by @herbelin | 2017-05-02 | ||
| | |/ / / / / / / | |/| | | | | | | | ||||
| | | | | * | | | | Fixing #5487 (v8.5 regression on ltac-matching expressions with evars). | 2017-05-01 | ||
| | | | | * | | | | Really fixing #2602 which was wrongly working because of #5487 hiding the cause. | 2017-05-01 | ||
| | | | | * | | | | Revert "Fixing #5487 (v8.5 regression on ltac-matching expressions with evars)." | 2017-04-28 | ||
| | | | | * | | | | Fixing #5487 (v8.5 regression on ltac-matching expressions with evars). | 2017-04-28 | ||
| * | | | | | | | | Post-rebase warnings (unused opens and 2 unused values) | 2017-04-27 | ||
| * | | | | | | | | Fix 4.04 warnings | 2017-04-27 | ||
| * | | | | | | | | Remove unused [open] statements | 2017-04-27 |