aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/cases.mli
Commit message (Expand)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* [api] A few more minor deprecation notices.Gravatar Emilio Jesus Gallego Arias2017-11-22
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* [general] Remove Econstr dependency from `intf`Gravatar Emilio Jesus Gallego Arias2017-10-25
* Efficient fresh name generation relying on sets.Gravatar Pierre-Marie Pédrot2017-09-28
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* A fix to #5414 (ident bound by ltac names now known for "match").Gravatar Hugo Herbelin2017-06-09
* [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
* Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\
* | Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
* | Making judgment type generic over the type of inner constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Cases API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| * Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-12-07
|/|
| * Fix UGraph.check_eq!Gravatar Matthieu Sozeau2016-11-30
* | Unify location handling of error functions.Gravatar Emilio Jesus Gallego Arias2016-08-19
|/
* Program: cleanup in cases, add optionsGravatar Matthieu Sozeau2016-06-29
* Revert "More abstraction in cases.mli."Gravatar Hugo Herbelin2016-04-27
* More abstraction in cases.mli.Gravatar Hugo Herbelin2016-04-27
* Fixing a "This clause is redundant" error when interpreting the "in"Gravatar Hugo Herbelin2016-04-27
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
|/
* Update headers.Gravatar Maxime Dénès2015-01-12
* 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
* - Fix the de Bruijn problem in check_projection for good :)Gravatar Matthieu Sozeau2014-06-17
* Removing dead code, thanks to new OCaml warnings and a bit of scripting.Gravatar Pierre-Marie Pédrot2014-04-23
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Fix compilation of pattern matching wrt variables: alias.Gravatar aspiwack2013-11-02
* Fix the compilation of pattern matching wrt to variables.Gravatar aspiwack2013-11-02
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* Modulification of nameGravatar ppedrot2012-12-18
* Modulification of identifierGravatar ppedrot2012-12-14
* Updating headers.Gravatar herbelin2012-08-08
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* remove many excessive open Util & Errors in mli'sGravatar letouzey2012-05-29
* Everything compiles again.Gravatar msozeau2012-03-14
* Second step of integration of Program:Gravatar msozeau2012-03-14
* Noise for nothingGravatar pboutill2012-03-02
* A bit of documentation around cases.ml + ML modules uselessly openGravatar herbelin2011-11-16
* 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
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Fix bug 2307Gravatar pboutill2010-05-20
* Some ocamldoc comments + Fixing name of .coqrc.version file in refmanGravatar pboutill2010-05-18
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Promote evar_defs to evar_map (in Evd)Gravatar glondu2009-11-11
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 04:26:07 +0000