aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/decl_mode/decl_interp.ml
Commit message (Expand)AuthorAge
* Farewell decl_modeGravatar Enrico Tassi2017-03-07
* Moving the Ltac plugin to a pack-based one.Gravatar Pierre-Marie Pédrot2017-02-17
* Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
* Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
* Unify location handling of error functions.Gravatar Emilio Jesus Gallego Arias2016-08-19
* closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)Gravatar Pierre Letouzey2016-07-03
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
* Supporting "(@foo) args" in patterns, where "@foo" has no arguments.Gravatar Hugo Herbelin2016-03-13
* The tactic generic argument now returns a value rather than a glob_expr.Gravatar Pierre-Marie Pédrot2016-02-22
* CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* Add syntax for naming new goals in refine: writing ?[id] instead of _Gravatar Hugo Herbelin2014-09-30
* Revert specific syntax for primitive projections, avoiding uglyGravatar Matthieu Sozeau2014-09-17
* 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
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Adding generic solvers to term holes. For now, no resolution mechanism norGravatar Pierre-Marie Pédrot2013-11-27
* More monomorphic List.mem + List.assoc + ...Gravatar letouzey2013-10-24
* Turn many List.assoc into List.assoc_fGravatar letouzey2013-10-24
* Removing a bunch of generic equalities.Gravatar ppedrot2013-09-27
* Removing more association lists in Constrintern.Gravatar ppedrot2013-09-02
* Removed the distinction between generic Ltac vars and Let/IntroGravatar ppedrot2013-06-27
* A uniformization step around understand_* and interp_* functions.Gravatar herbelin2013-05-09
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* Minor code cleaning in CArray / CList.Gravatar ppedrot2013-03-23
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* Modulification of identifierGravatar ppedrot2012-12-14
* Split Tacinterp in 3 files : Tacsubst, Tacintern and TacinterpGravatar letouzey2012-10-16
* 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
* Updating headers.Gravatar herbelin2012-08-08
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* Internalization of pattern is done in two phases.Gravatar pboutill2012-06-14
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* New files intf/constrexpr.mli and intf/notation_term.mli out of TopconstrGravatar letouzey2012-05-29
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
* Evar_kinds.mli containing former Evd.hole_kind, avoid deps on EvdGravatar letouzey2012-05-29
* Second step of integration of Program:Gravatar msozeau2012-03-14
* Noise for nothingGravatar pboutill2012-03-02
* Fixing bug #2640 and variants of it (inconsistency between when andGravatar herbelin2011-11-17
* Add a syntax entry for fully applied constructor patternGravatar pboutill2011-07-22
* s/raw/glob/g in decl_interp.ml for more consistencyGravatar glondu2010-12-24
* More {raw => glob} changes for consistencyGravatar glondu2010-12-24
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Change of nomenclature: rawconstr -> glob_constrGravatar glondu2010-12-23
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24