aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-05-24Merge PR#650: Fixing an extra bug with pattern_of_constrMaxime Dénès
2017-05-23unification.mli: Fix a spelling typo in a commentJason Gross
2017-05-19Fixing an extra bug with pattern_of_constr.Hugo Herbelin
2017-05-17Merge branch 'v8.6'Pierre-Marie Pédrot
2017-05-14Removing a line warned unused.Hugo Herbelin
2017-05-11Merge PR#594: An example showing the benefit of EconstrMaxime Dénès
2017-05-11Merge PR#373: A refined solution to the beta-iota discrepancies between 8.4 a...Maxime Dénès
2017-05-09Merge PR#606: Added an option Set Debug CbvMaxime Dénès
2017-05-05Remove dead code and unused open.Maxime Dénès
2017-05-05Merge PR#558: Adding a fold_glob_constr_with_binders combinatorMaxime Dénès
2017-05-05Upgrading some local function as a general-purpose combinator Option.List.map.Hugo Herbelin
2017-05-05Merge PR#544: Anonymous universesMaxime Dénès
2017-05-03Merge PR#404: patch for printing types of let bindingsMaxime Dénès
2017-05-03Added an option Set Debug Cbv.Hugo Herbelin
2017-05-03Type@{_} should not produce a flexible algebraic universe.Gaetan Gilbert
2017-05-03Allow flexible anonymous universes in instances and sorts.Gaetan Gilbert
2017-05-03Merge PR#411: Mention template polymorphism in the documentation.Maxime Dénès
2017-05-02applied the patch for printing types of let bindings by @herbelinAbhishek Anand (@brixpro-home)
2017-05-01Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).Hugo Herbelin
2017-05-01Really fixing #2602 which was wrongly working because of #5487 hiding the cause.Hugo Herbelin
2017-04-28Revert "Fixing #5487 (v8.5 regression on ltac-matching expressions with evars)."Maxime Dénès
2017-04-28Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).Hugo Herbelin
2017-04-27Post-rebase warnings (unused opens and 2 unused values)Gaetan Gilbert
2017-04-27Fix 4.04 warningsGaetan Gilbert
2017-04-27Remove unused [open] statementsGaetan Gilbert
2017-04-27Remove some unused values and typesGaetan Gilbert
2017-04-27Fix omitted labels in function callsGaetan Gilbert
2017-04-27A refined solution to the beta-iota discrepancies between 8.4 and 8.5 "refine".Hugo Herbelin
2017-04-27Merge branch 'v8.6'Pierre-Marie Pédrot
2017-04-25[location] [ast] Port module AST to CAstEmilio Jesus Gallego Arias
2017-04-25[location] Make location optional in Loc.locatedEmilio Jesus Gallego Arias
2017-04-25[location] Remove Loc.ghost.Emilio Jesus Gallego Arias
2017-04-24[location] Use located in misctypes.Emilio Jesus Gallego Arias
2017-04-24[location] Switch glob_constr to Loc.locatedEmilio Jesus Gallego Arias
2017-04-24[location] Move Glob_term.predicate_pattern to located.Emilio Jesus Gallego Arias
2017-04-24[location] Move Glob_term.cases_pattern to located.Emilio Jesus Gallego Arias
2017-04-24Merge PR#579: [flags] Deprecate is_silent/is_verbose in favor of single flag.Maxime Dénès
2017-04-21[flags] Deprecate is_silent/is_verbose in favor of single flag.Emilio Jesus Gallego Arias
2017-04-20Fix bug #5377: @? patterns broken.Pierre-Marie Pédrot
2017-04-19Fix bug #5476: Ltac has an inconsistent view of hypotheses.Pierre-Marie Pédrot
2017-04-15Merge branch 'v8.6' into trunkMaxime Dénès
2017-04-13Using fold_glob_constr_with_binders to code bound_glob_vars.Hugo Herbelin
2017-04-13Adding a fold_glob_constr_with_binders combinator.Hugo Herbelin
2017-04-13Silence a few OCaml warnings.Guillaume Melquiond
2017-04-11Merge PR#543: Sanitize instance interpretationMaxime Dénès
2017-04-11Update various comments to use "template polymorphism"Gaetan Gilbert
2017-04-11Merge PR#379: Introducing evar-insensitive constrsMaxime Dénès
2017-04-10Revert "refactoring: Reductionops.contextual_reduction_function type"Matej Košík
2017-04-10refactoring: Reductionops.contextual_reduction_function typeMatej Kosik
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 23:59:45 +0000