Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
| * | | | | | | | | 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 | ||
| * | | | | | | | | Remove some unused values and types | 2017-04-27 | ||
| * | | | | | | | | Fix omitted labels in function calls | 2017-04-27 | ||
| | | | * | | | | | A refined solution to the beta-iota discrepancies between 8.4 and 8.5 "refine". | 2017-04-27 | ||
| | |_|/ / / / / | |/| | | | | | | ||||
| * | | | | | | | Merge branch 'v8.6' | 2017-04-27 | ||
| |\ \ \ \ \ \ \ | | | |_|/ / / / | | |/| | | | | | ||||
* | | | | | | | | [location] [ast] Port module AST to CAst | 2017-04-25 | ||
* | | | | | | | | [location] Make location optional in Loc.located | 2017-04-25 | ||
* | | | | | | | | [location] Remove Loc.ghost. | 2017-04-25 | ||
* | | | | | | | | [location] Use located in misctypes. | 2017-04-24 | ||
* | | | | | | | | [location] Switch glob_constr to Loc.located | 2017-04-24 | ||
* | | | | | | | | [location] Move Glob_term.predicate_pattern to located. | 2017-04-24 | ||
* | | | | | | | | [location] Move Glob_term.cases_pattern to located. | 2017-04-24 | ||
|/ / / / / / / | ||||
* | | | | | | | Merge PR#579: [flags] Deprecate is_silent/is_verbose in favor of single flag. | 2017-04-24 | ||
|\ \ \ \ \ \ \ | ||||
| * | | | | | | | [flags] Deprecate is_silent/is_verbose in favor of single flag. | 2017-04-21 | ||
| | * | | | | | | Fix bug #5377: @? patterns broken. | 2017-04-20 | ||
* | | | | | | | | Fix bug #5476: Ltac has an inconsistent view of hypotheses. | 2017-04-19 | ||
|/ / / / / / / | ||||
* | | | | | | | Merge branch 'v8.6' into trunk | 2017-04-15 | ||
|\| | | | | | | ||||
| | | | | * | | Reinstate fixpoint refolding in [cbn], deactivated by mistake. | 2017-04-13 | ||
| | |_|_|/ / | |/| | | | | ||||
| | | * | | | Using fold_glob_constr_with_binders to code bound_glob_vars. | 2017-04-13 | ||
| | | * | | | Adding a fold_glob_constr_with_binders combinator. | 2017-04-13 | ||
* | | | | | | Silence a few OCaml warnings. | 2017-04-13 | ||
* | | | | | | Merge PR#543: Sanitize instance interpretation | 2017-04-11 | ||
|\ \ \ \ \ \ | |_|_|/ / / |/| | | | | | ||||
| | | * | | | Update various comments to use "template polymorphism" | 2017-04-11 | ||
| |_|/ / / |/| | | | | ||||
* | | | | | Merge PR#379: Introducing evar-insensitive constrs | 2017-04-11 | ||
|\ \ \ \ \ | ||||
* | | | | | | Revert "refactoring: Reductionops.contextual_reduction_function type" | 2017-04-10 | ||
* | | | | | | refactoring: Reductionops.contextual_reduction_function type | 2017-04-10 | ||
| | | * | | | Fixing #5460 (limitation in computing deps in pattern-matching compilation). | 2017-04-08 | ||
| | | | * | | Better support for printing constructors with let-ins. | 2017-04-07 | ||
| | | |/ / | ||||
| * | | | | Merge branch 'master' into econstr | 2017-04-07 | ||
| |\ \ \ \ | ||||
* | | | | | | Turning the printing primitive projection parameter flag off by default. | 2017-04-07 | ||
* | | | | | | Turning the printing primitive projection compatibility flag off by default. | 2017-04-07 | ||
| |/ / / / |/| | | | | ||||
* | | | | | Merge PR#508: Optimize pending evars | 2017-04-06 | ||
|\ \ \ \ \ | ||||
| | * | | | | Fix a normalization hotspot in computation of constr keys. | 2017-04-06 | ||
| | | * | | | Factor interp_instance out of Pretyping.pretype_global | 2017-04-06 | ||
| | | * | | | Avoid strange shadowing of Pretyping.interp_universe_level_name | 2017-04-06 | ||
| |_|/ / / |/| | | | | ||||
| | * | | | Removing a normalization hotspot from EConstr. | 2017-04-05 | ||
| | * | | | Merge branch 'trunk' into pr379 | 2017-04-04 | ||
| | |\ \ \ | |_|/ / / |/| | | | | ||||
| | * | | | Using delayed universe instances in EConstr. | 2017-04-01 | ||
| | * | | | Actually exporting delayed universes in the EConstr implementation. | 2017-04-01 | ||
| | * | | | Make the Constr.kind_of_term type parametric in sorts and universes. | 2017-03-31 | ||
| | * | | | Revert to incorrect heuristic in apply. | 2017-03-28 | ||
| | * | | | Fix interpretation of Ltac patterns episode 2. | 2017-03-24 | ||
| | * | | | Merge branch 'trunk' into pr379 | 2017-03-24 | ||
| | |\ \ \ | ||||
* | | | | | | Replacing "cast surgery" in LetIn by a proper field (see PR #404). | 2017-03-24 | ||
| |_|/ / / |/| | | | | ||||
| * | | | | Better algorithm for Evarconv.max_undefined_with_candidates. | 2017-03-24 | ||
* | | | | | Merge branch 'v8.6' into trunk | 2017-03-23 | ||
|\ \ \ \ \ | | |_|/ / | |/| | | | ||||
| * | | | | Intern names bound in match patterns | 2017-03-23 | ||
| | |_|/ | |/| | | ||||
| | * | | Make the computation of frozen evars lazy in Pretyping. | 2017-03-23 |