aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2017-06-16Fix a bugAmin Timany
2017-06-16Fix bugs and add an option for cumulativityAmin Timany
2017-06-16Fix bugsAmin Timany
2017-06-16Squashed commit of the following:Amin Timany
2017-06-16Make unification use subtyping info of inductivesAmin Timany
2017-06-16Use inductive subtyping for conv/cumulAmin Timany
2017-06-16Subtyping inference for inductoves and recordsAmin Timany
2017-06-16Using UInfoInd for universes in inductive typesAmin Timany
2017-06-15Merge PR#375: DeprecationMaxime Dénès
2017-06-14Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").Maxime Dénès
2017-06-14Deprecate options that were introduced for compatibility with 8.2.Guillaume Melquiond
2017-06-14Remove options deprecated since 8.4.Guillaume Melquiond
2017-06-14Remove support for Coq 8.3.Guillaume Melquiond
2017-06-14Remove support for Coq 8.2.Guillaume Melquiond
2017-06-13Merge PR#714: Print feature Proof-of-Concept (episode 2)Maxime Dénès
2017-06-09A fix to #5414 (ident bound by ltac names now known for "match").Hugo Herbelin
2017-06-08Merge branch 'v8.6'Pierre-Marie Pédrot
2017-06-06Remove the Sigma (monotonous state) API.Maxime Dénès
2017-06-06Merge PR#716: Don't double up on periods in anomaliesMaxime Dénès
2017-06-05Merge PR#590: A more explicit algebraic type for evars of kind MatchingVar + ...Maxime Dénès
2017-06-04Added support for a side effect on constants in reduction functions.Thomas Sibut-Pinote
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-06-02Don't double up on periods in anomaliesJason Gross
2017-06-01Merge PR#670: Postponing of universe constraints unification in term equality.Maxime Dénès
2017-06-01Merge PR#696: Trunk+cleanup constr of globalMaxime Dénès
2017-06-01Merge PR#561: Improving the Name APIMaxime Dénès
2017-06-01Merge PR#694: Fixing #5523 (missing support for complex constructions in recu...Maxime Dénès
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:38:40 +0000