aboutsummaryrefslogtreecommitdiff
path: root/parsing/egramcoq.ml
AgeCommit message (Expand)Author
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-02-16Removing non-marshallable data from the Agram constructor. Instead ofPierre-Marie Pédrot
2013-11-27Adding generic solvers to term holes. For now, no resolution mechanism norPierre-Marie Pédrot
2013-11-10Removing the dependency of every level of tactic ATSs on glob_tactic_expr.ppedrot
2013-11-09Revert the previous commit. It broke Coq compilation.ppedrot
2013-11-09Removing the dependency of every level of tactic ATSs on glob_tactic_expr.ppedrot
2013-11-09Moving notation types into grammar rule.ppedrot
2013-11-09Cleaning and documenting Egramcoq.ppedrot
2013-06-27Added a generic handler of Ltac quotations, based on the existingppedrot
2013-05-06States: frozen states can hold closuresgareuselesinge
2013-04-23Egramcoq+Lexer : no need for an init_functionletouzey
2013-04-23Egramcoq: clean an ugly code snippetletouzey
2013-04-22code simplifications concerning Summaryletouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 8)letouzey
2013-02-19Dir_path --> DirPathletouzey
2013-02-18use List.rev_map whenever possibleletouzey
2013-01-28Actually adding backtrace handling.ppedrot
2013-01-28Uniformization of the "anomaly" command.ppedrot
2012-12-18Modulification of nameppedrot
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-11-25Monomorphization (parsing)ppedrot
2012-11-15backtrack too much commited files in the last commit.courtieu
2012-11-15Fixing emacs diff bug with .dir-locals.el.courtieu
2012-11-08Monomorphized a lot of equalities over OCaml integers, thanks toppedrot
2012-10-05Fix a confusion between types of locations in an untyped part of the parserletouzey
2012-10-04Adding a nominal typing layer to Metasyntax in order to clarifyppedrot
2012-10-04Moved Compat to parsing. This permits to break the dependency of theppedrot
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-09-17More cleaning on Utils and CList. Some parts of the code beingppedrot
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-08-08Updating headers.herbelin
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-06-14Internalization of pattern is done in two phases.pboutill
2012-05-29Split Egrammar into Egramml and Egramcoqletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 16:27:12 +0000