aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernacentries.ml
Commit message (Expand)AuthorAge
* Update headers.Gravatar Maxime Dénès2015-01-12
* In Show Universes, print universes before normalization.Gravatar Matthieu Sozeau2015-01-05
* Proof using: do not clear letins (unless they use a cleared var)Gravatar Enrico Tassi2014-12-29
* Proof using: call "clear" to remove from sight the vars not selectedGravatar Enrico Tassi2014-12-28
* remove debug prints (leftover)Gravatar Enrico Tassi2014-12-28
* Better doc and a few fixes for Proof using.Gravatar Enrico Tassi2014-12-19
* Proof using: New vernacular to name sets of section variablesGravatar Enrico Tassi2014-12-18
* Arguments: warn only if no option is given (Close 3860)Gravatar Enrico Tassi2014-12-17
* Fixing CAMLP4 compilation.Gravatar Pierre-Marie Pédrot2014-12-16
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
* Error messages of Searchxxx are coherent with goal selector.Gravatar Pierre Courtieu2014-12-16
* About now accepts hypothesis names and goal selector.Gravatar Pierre Courtieu2014-12-15
* Util.un_op -> Option.defaultGravatar Pierre Boutillier2014-12-14
* Searchxxx now interpret patterns in goal environment if any.Gravatar Pierre Courtieu2014-12-12
* Searchxxx now search also the hypothesis and support goal selector.Gravatar Pierre Courtieu2014-12-12
* Reactivating option "Set Printing Existential Instances" for asking printing ...Gravatar Hugo Herbelin2014-12-04
* Now that evars can be parsed, protect strongly Check from calling kernel with...Gravatar Hugo Herbelin2014-11-03
* Show: do print the goalsGravatar Enrico Tassi2014-11-03
* Add an [Info Level] option to print info traces automatically.Gravatar Arnaud Spiwack2014-11-01
* Add [Info] command.Gravatar Arnaud Spiwack2014-11-01
* Show_script called only if in coqtop modeGravatar Enrico Tassi2014-10-31
* Fixes for PG (Close 3763, 3770)Gravatar Enrico Tassi2014-10-27
* Change reduction_of_red_expr to return an e_reduction_function returningGravatar Matthieu Sozeau2014-10-24
* Goal printing made uniform: always done in STM (close 3585)Gravatar Enrico Tassi2014-10-22
* Continuing experimental printing of the signature of open evars inGravatar Hugo Herbelin2014-10-21
* Experimental printing of the signature of open evars in Check.Gravatar Hugo Herbelin2014-10-17
* 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
* Splitting out of auto.ml a file hints.ml dedicated to hints so as toGravatar Hugo Herbelin2014-10-07
* Notation: option to attach extra pretty printing rules to notationsGravatar Enrico Tassi2014-09-29
* Revert specific syntax for primitive projections, avoiding uglyGravatar Matthieu Sozeau2014-09-17
* Rework typeclass resolution and control of backtracking.Gravatar Matthieu Sozeau2014-09-15
* 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
* 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 [Variant] and [Record] really don't accept the wrong kind of...Gravatar Arnaud Spiwack2014-09-04
* Print [Variant] types with the keyword [Variant].Gravatar Arnaud Spiwack2014-09-04
* Moving code of tactic interpretation from Tacenv to Vernacentries.Gravatar Pierre-Marie Pédrot2014-08-31
* Fixing the essence of naming bug #3204: use same strategy for namingGravatar Hugo Herbelin2014-08-25
* STM: new "par:" goal selector, like "all:" but in parallelGravatar Enrico Tassi2014-08-05
* Unifying locate code, also making it more powerful: it is now able to findGravatar Pierre-Marie Pédrot2014-07-21
* Adding a new "Locate Term" command, distinct from the raw "Locate" command.Gravatar Pierre-Marie Pédrot2014-07-21
* More complete printing of Ltac location, akin to the term-dedicated Locate co...Gravatar Pierre-Marie Pédrot2014-07-21
* smartlocate: look for the head symbol for realGravatar Enrico Tassi2014-07-14
* Adding a "time" tactical for benchmarking purposes. In case the tacticGravatar Hugo Herbelin2014-07-13
* Revert "time tac" (committed by mistake).Gravatar Hugo Herbelin2014-07-07
* time tacGravatar Hugo Herbelin2014-07-07
* Add toplevel commands to declare global universes and constraints.Gravatar Matthieu Sozeau2014-07-01
* all coqide specific files moved into ide/Gravatar Enrico Tassi2014-06-25
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 21:15:40 +0000