aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2014-11-22Removing superfluous newlines in setoid_rewrite error message.Hugo Herbelin
2014-11-20Exporting the function handling side-effects only applied to terms.Pierre-Marie Pédrot
2014-11-18Fixing a little bug with nested but convertible occurrences in "destruct at".Hugo Herbelin
2014-11-17Setting error tag on generic errors returned by Coqtop.Pierre-Marie Pédrot
2014-11-16For consistency with other coqtop flags, use -help rather than --help in usage.Hugo Herbelin
2014-11-15Removing a pperrnl.Pierre-Marie Pédrot
2014-11-15Adding a command line option to print out accepted color tags.Pierre-Marie Pédrot
2014-11-15Reworking the -color flag of coqtop.Pierre-Marie Pédrot
2014-11-15Plugging the color initialization in the Coqtop loop.Pierre-Marie Pédrot
2014-11-14Exit with code 129 when an anomaly occurs.Xavier Clerc
2014-11-13Fixing Scheme Equality, after bug introduced in bf018569405c.Hugo Herbelin
2014-11-08Continuing 3741c46fe134 on reporting ltac error.Hugo Herbelin
2014-11-03Now that evars can be parsed, protect strongly Check from calling kernel with...Hugo Herbelin
2014-11-03Show: do print the goalsEnrico Tassi
2014-11-01Add an [Info Level] option to print info traces automatically.Arnaud Spiwack
2014-11-01Add [Info] command.Arnaud Spiwack
2014-10-31STM: new worker for queriesEnrico Tassi
2014-10-31Show_script called only if in coqtop modeEnrico Tassi
2014-10-27Fixes for PG (Close 3763, 3770)Enrico Tassi
2014-10-25This commit introduces changes in induction and destruct.Hugo Herbelin
2014-10-24Change reduction_of_red_expr to return an e_reduction_function returningMatthieu Sozeau
2014-10-23Evd.future_goals: forgot to revert the list in two places.Arnaud Spiwack
2014-10-22Make rint_location_in_file resilient to Cd (close 3630)Enrico Tassi
2014-10-22Goal printing made uniform: always done in STM (close 3585)Enrico Tassi
2014-10-22Split [Proofview] into a file where the basic operations on the state are def...Arnaud Spiwack
2014-10-22Proofview: move more functions to the Unsafe module.Arnaud Spiwack
2014-10-22Remove the deprecated open-constr based refine.Arnaud Spiwack
2014-10-22Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.Arnaud Spiwack
2014-10-21Continuing experimental printing of the signature of open evars inHugo Herbelin
2014-10-17Now printing "now a keyword" only in verbose mode.Hugo Herbelin
2014-10-17Experimental printing of the signature of open evars in Check.Hugo Herbelin
2014-10-14Fix ML paths (thanks Jean-Marc Notin for bisecting it)Enrico Tassi
2014-10-13Fix typo, thanks Mike Shulman for spotting itEnrico Tassi
2014-10-13Emit a warning for void Arguments statement (Close 3713)Enrico Tassi
2014-10-13STM: primitives to snapshot a .vi while in interactive modeEnrico Tassi
2014-10-13library/opaqueTables: enable their use in interactive modeEnrico Tassi
2014-10-13Coqinit: look in toploop/ even if configured with -localEnrico Tassi
2014-10-11Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameMatthieu Sozeau
2014-10-10Give the same argument name for the record binder of type classMatthieu Sozeau
2014-10-10Add debug printers for projections, fix printing of evar constraintsMatthieu Sozeau
2014-10-07Splitting out of auto.ml a file hints.ml dedicated to hints so as toHugo Herbelin
2014-10-03Fixing #3193 (honoring implicit arguments in local definitions).Hugo Herbelin
2014-10-03Fixing #3634 (wrong env in "cannot instantiate because not in itsHugo Herbelin
2014-10-02Implement module subtyping for polymorphic constants (errors onMatthieu Sozeau
2014-10-02Print type and environment of unsolved holes.Arnaud Spiwack
2014-10-01Fixing nice printing of error reporting with ml tactics bound to ltac names.Hugo Herbelin
2014-09-30Add syntax for naming new goals in refine: writing ?[id] instead of _Hugo Herbelin
2014-09-29Notation: option to attach extra pretty printing rules to notationsEnrico Tassi
2014-09-29do not explode if a plugin is not up to date on -help (Close: 3673)Enrico Tassi
2014-09-29Merging some functions from evarutil.ml/evd.ml.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 10:08:53 +0000