aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/cases.mli
Commit message (Expand)AuthorAge
* 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
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Notation concise pour la valeur par défaut des cas reconnus commeGravatar herbelin2008-05-28
* Mise en place d'un algorithme d'inversion des contraintes de type lorsGravatar herbelin2008-05-05
* - Second pass on implementation of let pattern. Parse "let ' par [as x]?Gravatar msozeau2008-03-28
* Add new LetPattern construct to replace dest. syntax: let| pat := t in b is b...Gravatar msozeau2008-01-17
* Various Program fixes, multiple pattern matches, aliases. Fix bug in coercion...Gravatar msozeau2007-06-09
* - Utilisation d'abbréviations pour les types intervenant dans RCasesGravatar herbelin2006-04-26
* Made pretyping a functor over a coercion implementation. Pretyping.Default us...Gravatar msozeau2006-03-22
* Suppression fonctions d'interprétation du vieux CaseGravatar herbelin2006-01-30
* Gestion des erreurs pour nombre incorrect d'argument des constructeurs (et deGravatar herbelin2006-01-30
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* deuxieme vague de modifs: evar_defs fonctionnelGravatar barras2004-09-07
* Nouvelle en-têteGravatar herbelin2004-07-16
* Suppression de Rawterm.loc, branchement sur Util.locGravatar herbelin2004-07-16
* Deplacement subst_rawconstr dans RawtermGravatar herbelin2003-11-19
* Nouvelle mouture du traducteur v7->v8Gravatar herbelin2003-08-11
* petit nettoyage de kernel/inductiveGravatar barras2002-02-07
* Nettoyage exceptions liées au vieux CaseGravatar herbelin2001-12-18
* Simplification de la propagation du prédicat, bugs, et messages d'erreursGravatar herbelin2001-11-21
* Suppression des local_constraints, des ctxtty et du focus.Gravatar clrenard2001-11-06