aboutsummaryrefslogtreecommitdiff
path: root/vernac/vernacentries.ml
AgeCommit message (Expand)Author
2017-06-16Change the option to Set Inductive CumulativityAmin Timany
2017-06-16Correct coqchk reductionAmin Timany
2017-06-16Fix bugs and add an option for cumulativityAmin Timany
2017-06-15Merge PR#769: [lib] Remove obsolete state-management function add_frozen_stateMaxime Dénès
2017-06-15Merge PR#375: DeprecationMaxime Dénès
2017-06-14Merge PR#763: [proof] Deprecate redundant wrappers.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-12[lib] Remove obsolete state-management function add_frozen_stateEmilio Jesus Gallego Arias
2017-06-12Remove Show Thesis command which was never implemented.Théo Zimmermann
2017-06-12Remove non-working Show Tree and Show Node commands.Théo Zimmermann
2017-06-12Remove Show Implicit Arguments command.Théo Zimmermann
2017-06-11[proof] Deprecate redundant wrappers.Emilio Jesus Gallego Arias
2017-06-08Merge branch 'v8.6'Pierre-Marie Pédrot
2017-06-07Merge PR#717: [proof] Deprecate "proof mode" APIMaxime Dénès
2017-06-06Remove the Sigma (monotonous state) API.Maxime Dénès
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-06-01Merge PR#696: Trunk+cleanup constr of globalMaxime Dénès
2017-05-31[proof] Deprecate "proof mode" APIEmilio Jesus Gallego Arias
2017-05-31Creating a module Nameops.Name extending module Names.Name.Hugo Herbelin
2017-05-29Cleanup: removal of constr_of_global.Matthieu Sozeau
2017-05-27[cleanup] Unify all calls to the error function.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-19Removing unused warnings.Pierre-Marie Pédrot
2017-05-19Merge branch 'master' into ltac2-hooksPierre-Marie Pédrot
2017-05-05Adapted to EConstr.Pierre Courtieu
2017-05-03Allowing to pass arbitrary data in internalization environments.Pierre-Marie Pédrot
2017-05-03Adding an even more compact mode for goal display.Pierre Courtieu
2017-04-28Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l...Maxime Dénès
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-24Merge PR#579: [flags] Deprecate is_silent/is_verbose in favor of single flag.Maxime Dénès
2017-04-21Remove VernacErrorGaetan Gilbert
2017-04-21[flags] Deprecate is_silent/is_verbose in favor of single flag.Emilio Jesus Gallego Arias
2017-04-15Merge branch 'v8.6' into trunkMaxime Dénès
2017-04-12Merge PR#441: Port Toplevel to the Stm APIMaxime Dénès
2017-04-12[flags] Documentation and a minor tweak.Emilio Jesus Gallego Arias
2017-04-12[vernac] vernacentries.mli cleanupEmilio Jesus Gallego Arias
2017-04-09Removing internal support for accepting "{struct x}" and co in "Theorem with".Hugo Herbelin
2017-04-04Merge branch 'trunk' into pr379Maxime Dénès
2017-03-30Merge PR#511: [stm] Remove some obsolete vernacs/classification.Maxime Dénès
2017-03-24Merge branch 'trunk' into pr379Maxime Dénès
2017-03-24[stm] Remove some obsolete vernacs/classification.Emilio Jesus Gallego Arias
2017-03-24[nit] Fix a couple incorrect uses of msg_error.Emilio Jesus Gallego Arias
2017-03-21[pp] Remove uses of expensive string_of_ppcmds.Emilio Jesus Gallego Arias
2017-03-21[pp] [ide] Minor cleanups in pp code.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 10:56:32 +0000