aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
Commit message (Expand)AuthorAge
* Allowing (Co)Fixpoint to be defined local and Let-style.Gravatar ppedrot2013-03-11
* Added a Local Definition vernacular command. This type of definitionGravatar ppedrot2013-03-11
* avoid (Int.equal (cmp ...) 0) when a boolean equality existsGravatar letouzey2013-02-19
* Dir_path --> DirPathGravatar letouzey2013-02-19
* Removing Exc_located and using the new exception enrichementGravatar ppedrot2013-02-18
* use List.rev_map whenever possibleGravatar letouzey2013-02-18
* Useless use of hooks in VernacDefinition. In addition, this wasGravatar ppedrot2013-02-10
* Actually adding backtrace handling.Gravatar ppedrot2013-01-28
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
* Avoiding collision between Camlp4 Loc.Exc_located and Coq's Loc.Exc_located.Gravatar herbelin2012-12-22
* Yet a new reduction tactic in Coq : cbnGravatar pboutill2012-12-21
* Modulification of nameGravatar ppedrot2012-12-18
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Modulification of identifierGravatar ppedrot2012-12-14
* Early translation of camlp4/camlp5 located errors into coq-locatedGravatar herbelin2012-12-04
* Monomorphization (parsing)Gravatar ppedrot2012-11-25
* backtrack too much commited files in the last commit.Gravatar courtieu2012-11-15
* Fixing emacs diff bug with .dir-locals.el.Gravatar courtieu2012-11-15
* More monomorphizationsGravatar ppedrot2012-11-13
* Monomorphized a lot of equalities over OCaml integers, thanks toGravatar ppedrot2012-11-08
* Fix reference_or_constr grammar rule to accept @t as a constrGravatar gareuselesinge2012-11-07
* Change [Hints Resolve] to still accept constrs as argumentsGravatar msozeau2012-10-31
* Fixed #2926:Gravatar ppedrot2012-10-29
* Change Hint Resolve, Immediate to take a global reference as argumentGravatar msozeau2012-10-26
* Split Tacinterp in 3 files : Tacsubst, Tacintern and TacinterpGravatar letouzey2012-10-16
* Egramml: minor simplificationGravatar letouzey2012-10-15
* restore compatibility with camlp5 < 6.00Gravatar letouzey2012-10-06
* still some more dead code removalGravatar letouzey2012-10-06
* remove useless hidden_flag in TacMutual(Co)FixGravatar letouzey2012-10-06
* Fix a confusion between types of locations in an untyped part of the parserGravatar letouzey2012-10-05
* Adding a nominal typing layer to Metasyntax in order to clarifyGravatar ppedrot2012-10-04
* Moved Compat to parsing. This permits to break the dependency of theGravatar ppedrot2012-10-04
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* avoid referring to Term in constrexpr.mli and glob_term.mliGravatar letouzey2012-10-02
* Added a new tactical infoH tac, that displays the names of hypothesis created...Gravatar courtieu2012-10-01
* More cleanup of Util: utf8 aspects moved to a new file unicode.mlGravatar letouzey2012-09-18
* More cleaning on Utils and CList. Some parts of the code beingGravatar ppedrot2012-09-17
* Partial revert of Yann commit in order to use CLib.List when openingGravatar ppedrot2012-09-14
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* The new ocaml compiler (4.00) has a lot of very cool warnings,Gravatar regisgia2012-09-14
* Added support for option Local (at module level) in Tactic Notation.Gravatar herbelin2012-08-11
* Updating headers.Gravatar herbelin2012-08-08
* Bigint: new functions of_int and to_int, 2nd arg of pow in intGravatar letouzey2012-08-02
* Getting rid of the undocumented [complete] tactic, which wasGravatar ppedrot2012-07-19
* Re-allow Reset in compiled filesGravatar letouzey2012-07-11
* destruct: full compatibility with former _eqn syntaxGravatar letouzey2012-07-09
* The tactic remember now accepts a final eqn:H option (grant wish #2489)Gravatar letouzey2012-07-09
* induction/destruct : nicer syntax for generating equations (solves #2741)Gravatar letouzey2012-07-09