aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* 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
* toploop plugins taken into account when printing --help (close: 3535)Gravatar Enrico Tassi2014-09-09
* Removing dead code relative to the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
* Parsing of Type@{max(i,j)}.Gravatar Matthieu Sozeau2014-09-08
* Fixing bug #3492.Gravatar Pierre-Marie Pédrot2014-09-07
* Renaming goal-entering functions.Gravatar Pierre-Marie Pédrot2014-09-06
* More explicit printing in Himsg.Gravatar Pierre-Marie Pédrot2014-09-04
* Commands like [Inductive > X := … | … | …] raise an error message inste...Gravatar Arnaud Spiwack2014-09-04
* Remove [Infer] option of records.Gravatar Arnaud Spiwack2014-09-04
* Type definitions with [Variant] don't generate inductive schemes by default.Gravatar Arnaud Spiwack2014-09-04
* Type definitions [Variant] and [Record] really don't accept the wrong kind of...Gravatar Arnaud Spiwack2014-09-04
* Types declared as Variants really do not accept recursive definitions.Gravatar Arnaud Spiwack2014-09-04
* Print [Variant] types with the keyword [Variant].Gravatar Arnaud Spiwack2014-09-04
* Print error messages with more hidden information based on α-equivalence .Gravatar Arnaud Spiwack2014-09-03
* Additional entry tactic_arg in Print Grammar tactic.Gravatar Pierre-Marie Pédrot2014-09-03
* coqworkmgrGravatar Enrico Tassi2014-09-02
* Getting rid of atomic tactics in Tacenv.Gravatar Pierre-Marie Pédrot2014-08-31
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 01:22:48 +0000