aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* Fixes for PG (Close 3763, 3770)Gravatar Enrico Tassi2014-10-27
* This commit introduces changes in induction and destruct.Gravatar Hugo Herbelin2014-10-25
* Change reduction_of_red_expr to return an e_reduction_function returningGravatar Matthieu Sozeau2014-10-24
* Evd.future_goals: forgot to revert the list in two places.Gravatar Arnaud Spiwack2014-10-23
* Make rint_location_in_file resilient to Cd (close 3630)Gravatar Enrico Tassi2014-10-22
* Goal printing made uniform: always done in STM (close 3585)Gravatar Enrico Tassi2014-10-22
* Split [Proofview] into a file where the basic operations on the state are def...Gravatar Arnaud Spiwack2014-10-22
* Proofview: move more functions to the Unsafe module.Gravatar Arnaud Spiwack2014-10-22
* Remove the deprecated open-constr based refine.Gravatar Arnaud Spiwack2014-10-22
* Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.Gravatar Arnaud Spiwack2014-10-22
* Continuing experimental printing of the signature of open evars inGravatar Hugo Herbelin2014-10-21
* Now printing "now a keyword" only in verbose mode.Gravatar Hugo Herbelin2014-10-17
* Experimental printing of the signature of open evars in Check.Gravatar Hugo Herbelin2014-10-17
* Fix ML paths (thanks Jean-Marc Notin for bisecting it)Gravatar Enrico Tassi2014-10-14
* Fix typo, thanks Mike Shulman for spotting itGravatar Enrico Tassi2014-10-13
* Emit a warning for void Arguments statement (Close 3713)Gravatar Enrico Tassi2014-10-13
* STM: primitives to snapshot a .vi while in interactive modeGravatar Enrico Tassi2014-10-13
* library/opaqueTables: enable their use in interactive modeGravatar Enrico Tassi2014-10-13
* Coqinit: look in toploop/ even if configured with -localGravatar Enrico Tassi2014-10-13
* Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameGravatar Matthieu Sozeau2014-10-11
* Give the same argument name for the record binder of type classGravatar Matthieu Sozeau2014-10-10
* Add debug printers for projections, fix printing of evar constraintsGravatar Matthieu Sozeau2014-10-10
* Splitting out of auto.ml a file hints.ml dedicated to hints so as toGravatar Hugo Herbelin2014-10-07
* Fixing #3193 (honoring implicit arguments in local definitions).Gravatar Hugo Herbelin2014-10-03
* Fixing #3634 (wrong env in "cannot instantiate because not in itsGravatar Hugo Herbelin2014-10-03
* Implement module subtyping for polymorphic constants (errors onGravatar Matthieu Sozeau2014-10-02
* Print type and environment of unsolved holes.Gravatar Arnaud Spiwack2014-10-02
* Fixing nice printing of error reporting with ml tactics bound to ltac names.Gravatar Hugo Herbelin2014-10-01
* Add syntax for naming new goals in refine: writing ?[id] instead of _Gravatar Hugo Herbelin2014-09-30
* Notation: option to attach extra pretty printing rules to notationsGravatar Enrico Tassi2014-09-29
* do not explode if a plugin is not up to date on -help (Close: 3673)Gravatar Enrico Tassi2014-09-29
* Merging some functions from evarutil.ml/evd.ml.Gravatar Hugo Herbelin2014-09-29
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
* Fixing bug #3646.Gravatar Pierre-Marie Pédrot2014-09-19
* mltop: when a plugin is loaded store its full path in the summaryGravatar Enrico Tassi2014-09-18
* Be more conservative and keep the use of eq_constr in pretyping/ functions.Gravatar Matthieu Sozeau2014-09-17
* Fix bug #3593, making constr_eq and progress work up toGravatar Matthieu Sozeau2014-09-17
* Revert specific syntax for primitive projections, avoiding uglyGravatar Matthieu Sozeau2014-09-17
* Undo prints only if coqtop || emacsGravatar Enrico Tassi2014-09-16
* better error messageGravatar Enrico Tassi2014-09-16
* Rework typeclass resolution and control of backtracking.Gravatar Matthieu Sozeau2014-09-15
* Providing a -type-in-type option for collapsing the universe hierarchy.Gravatar Hugo Herbelin2014-09-13
* Uniformisation of the order of arguments env and sigma.Gravatar Hugo Herbelin2014-09-12
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* Add a flag for restricting resolution of typeclasses toGravatar Matthieu Sozeau2014-09-11
* Fix categorization of recursive inductives.Gravatar Matthieu Sozeau2014-09-10
* Fixing localisation of tactic errors (my mistake in himsg.ml essentially).Gravatar Hugo Herbelin2014-09-10
* VernacExtend does not dispatch on type anymore.Gravatar Pierre-Marie Pédrot2014-09-10
* Load Prelude.vi if not Prelude.vo is found (Close: 3595)Gravatar Enrico Tassi2014-09-09
* Undo: if the ui is coqtop (command line) then Undo is not part of the doc.Gravatar Enrico Tassi2014-09-09
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 09:22:13 +0000