aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2017-05-31Merge PR#560: Reinstate fixpoint refolding in [cbn], deactivated by mistake (...Maxime Dénès
2017-05-31Using a more explicit algebraic type for evars of kind "MatchingVar".Hugo Herbelin
2017-05-31Creating a module Nameops.Name extending module Names.Name.Hugo Herbelin
2017-05-31Fixing #5523 (missing support for complex constructions in recursive notations).Hugo Herbelin
2017-05-30Support for using type information to infer more precise evar sources.Hugo Herbelin
2017-05-29Pretyping cleanup: remove constr_of_global callsMatthieu Sozeau
2017-05-29Merge PR#546: Fix for bug #4499 and other minor related bugsMaxime Dénès
2017-05-29Merge PR#512: [cleanup] Unify all calls to the error function.Maxime Dénès
2017-05-27[cleanup] Unify all calls to the error function.Emilio Jesus Gallego Arias
2017-05-27[coqlib] Move `Coqlib` to `library/`.Emilio Jesus Gallego Arias
2017-05-25Merge PR#608: Allow Ltac2 as a pluginMaxime Dénès
2017-05-25Merge PR#481: [option] Remove support for non-synchronous options.Maxime Dénès
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-05-24[option] Remove support for non-synchronous options.Emilio 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-23Postponing of universe constraints unification in term equality.Pierre-Marie Pédrot
2017-05-19Fixing an extra bug with pattern_of_constr.Hugo Herbelin
2017-05-19Merge branch 'master' into ltac2-hooksPierre-Marie Pédrot
2017-05-17fix swapping of ids in tuples, bug 5486Paul Steckler
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-03Generalizing the tactic-in-term embedding to any generic argument.Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-04 18:50:29 +0000