aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/typing.mli
Commit message (Expand)AuthorAge
* [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
* Removing various compatibility layers of tactics.Gravatar Pierre-Marie Pédrot2017-02-14
* Removing compatibility layers in RetypingGravatar Pierre-Marie Pédrot2017-02-14
* Clenv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Making judgment type generic over the type of inner constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Typing API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-09-14
|\
| * Fixing #5077 (failure on typing a fixpoint with evars in its type).Gravatar Hugo Herbelin2016-09-10
* | Renaming functions in Typing to stick to the standard e_* scheme.Gravatar Pierre-Marie Pédrot2016-02-15
|/
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Safer typing primitives.Gravatar Pierre-Marie Pédrot2015-05-13
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Update headers.Gravatar Maxime Dénès2015-01-12
* Proofview refiner is now type-safe by default.Gravatar Pierre-Marie Pédrot2014-09-04
* Typing.sort_of does not leak evarmaps anymore.Gravatar Pierre-Marie Pédrot2014-09-04
* Fix bug #3559, ensuring a canonical order of universe level quantifications whenGravatar Matthieu Sozeau2014-09-04
* Refresh universes for Ltac's type_of, as the term can be used anywhere,Gravatar Matthieu Sozeau2014-05-09
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* A more informative message when the elimination predicate forGravatar herbelin2013-02-17
* Updating headers.Gravatar herbelin2012-08-08
* More unification in type_of and addition of e_type_of to get the newGravatar herbelin2011-10-24
* Applied the trick of Chung-Kil Hur to solve second-order matchingGravatar herbelin2011-10-10
* It happens that the type inference algorithm (pretyping) did not checkGravatar herbelin2011-10-05
* 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
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Added a function in typing.ml to solve evars of a constr w/o going back down ...Gravatar herbelin2010-04-05
* Promote evar_defs to evar_map (in Evd)Gravatar glondu2009-11-11
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* restructuration des printers: proofs passe avant parsingGravatar barras2004-09-17
* hiding the meta_map in evar_defsGravatar barras2004-09-15
* premiere reorganisation de l\'unificationGravatar barras2004-09-03
* Nouvelle en-têteGravatar herbelin2004-07-16
* Suppression des local_constraints, des ctxtty et du focus.Gravatar clrenard2001-11-06
* entetesGravatar filliatr2001-03-15
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* mise au point Declare et avancee dans AsttermGravatar filliatr1999-12-01
* - environment -> safe_environmentGravatar filliatr1999-12-01
* - Typing -> Safe_typingGravatar filliatr1999-12-01
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 02:48:23 +0000