aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* [location] [ast] Port module AST to CAstGravatar Emilio Jesus Gallego Arias2017-04-25
* [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
* [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
* [location] Use located in misctypes.Gravatar Emilio Jesus Gallego Arias2017-04-24
* [location] Switch glob_constr to Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-24
* [location] Move Glob_term.predicate_pattern to located.Gravatar Emilio Jesus Gallego Arias2017-04-24
* [location] Move Glob_term.cases_pattern to located.Gravatar Emilio Jesus Gallego Arias2017-04-24
* Merge PR#579: [flags] Deprecate is_silent/is_verbose in favor of single flag.Gravatar Maxime Dénès2017-04-24
|\
| * [flags] Deprecate is_silent/is_verbose in favor of single flag.Gravatar Emilio Jesus Gallego Arias2017-04-21
* | Fix bug #5476: Ltac has an inconsistent view of hypotheses.Gravatar Pierre-Marie Pédrot2017-04-19
|/
* Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-04-15
|\
* | Silence a few OCaml warnings.Gravatar Guillaume Melquiond2017-04-13
* | Merge PR#543: Sanitize instance interpretationGravatar Maxime Dénès2017-04-11
|\ \
* \ \ Merge PR#379: Introducing evar-insensitive constrsGravatar Maxime Dénès2017-04-11
|\ \ \
* | | | Revert "refactoring: Reductionops.contextual_reduction_function type"Gravatar Matej Košík2017-04-10
* | | | refactoring: Reductionops.contextual_reduction_function typeGravatar Matej Kosik2017-04-10
| | | * Fixing #5460 (limitation in computing deps in pattern-matching compilation).Gravatar Hugo Herbelin2017-04-08
| * | | Merge branch 'master' into econstrGravatar Pierre-Marie Pédrot2017-04-07
| |\ \ \
* | | | | Turning the printing primitive projection parameter flag off by default.Gravatar Hugo Herbelin2017-04-07
* | | | | Turning the printing primitive projection compatibility flag off by default.Gravatar Hugo Herbelin2017-04-07
| |/ / / |/| | |
* | | | Merge PR#508: Optimize pending evarsGravatar Maxime Dénès2017-04-06
|\ \ \ \
| | * | | Fix a normalization hotspot in computation of constr keys.Gravatar Pierre-Marie Pédrot2017-04-06
| | | * | Factor interp_instance out of Pretyping.pretype_globalGravatar Gaetan Gilbert2017-04-06
| | | * | Avoid strange shadowing of Pretyping.interp_universe_level_nameGravatar Gaetan Gilbert2017-04-06
| |_|/ / |/| | |
| | * | Removing a normalization hotspot from EConstr.Gravatar Pierre-Marie Pédrot2017-04-05
| | * | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-04-04
| | |\ \ | |_|/ / |/| | |
| | * | Using delayed universe instances in EConstr.Gravatar Pierre-Marie Pédrot2017-04-01
| | * | Actually exporting delayed universes in the EConstr implementation.Gravatar Pierre-Marie Pédrot2017-04-01
| | * | Make the Constr.kind_of_term type parametric in sorts and universes.Gravatar Pierre-Marie Pédrot2017-03-31
| | * | Revert to incorrect heuristic in apply.Gravatar Maxime Dénès2017-03-28
| | * | Fix interpretation of Ltac patterns episode 2.Gravatar Maxime Dénès2017-03-24
| | * | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
| | |\ \
* | | | | Replacing "cast surgery" in LetIn by a proper field (see PR #404).Gravatar Hugo Herbelin2017-03-24
| |_|/ / |/| | |
| * | | Better algorithm for Evarconv.max_undefined_with_candidates.Gravatar Pierre-Marie Pédrot2017-03-24
* | | | Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-03-23
|\ \ \ \ | | |_|/ | |/| |
| * | | Intern names bound in match patternsGravatar Tej Chajed2017-03-23
| | * | Make the computation of frozen evars lazy in Pretyping.Gravatar Pierre-Marie Pédrot2017-03-23
| | * | Fast path in computation of frozen evars in Pretyping.Gravatar Pierre-Marie Pédrot2017-03-23
| | * | Ensuring static invariants about handling of pending evars in Pretyping.Gravatar Pierre-Marie Pédrot2017-03-23
| |/ / |/| |
* | | Merge PR#437: Improve unification debug trace.Gravatar Maxime Dénès2017-03-17
|\ \ \
| | | * Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
| | | |\ | |_|_|/ |/| | |
| | | * Quick hack to fix interpretation of patterns in Ltac.Gravatar Pierre-Marie Pédrot2017-02-14
| | | * Dedicated datatype for aliases in Evarsolve.Gravatar Pierre-Marie Pédrot2017-02-14
| | | * Putting back the occur_meta_or_undefined_evar function in the old term API.Gravatar Pierre-Marie Pédrot2017-02-14
| | | * Namegen primitives now apply on evar constrs.Gravatar Pierre-Marie Pédrot2017-02-14
| | | * Moving printing code from Evd to Termops.Gravatar Pierre-Marie Pédrot2017-02-14
| | | * Chasing a few unsafe constr coercions.Gravatar Pierre-Marie Pédrot2017-02-14
| | | * Putting back the subst_defined_metas_evars function in the old term API.Gravatar Pierre-Marie Pédrot2017-02-14
| | | * Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
| | | * Introducing contexts parameterized by the inner term type.Gravatar Pierre-Marie Pédrot2017-02-14