aboutsummaryrefslogtreecommitdiff
path: root/pretyping/retyping.mli
AgeCommit message (Expand)Author
2020-07-05Fix Canonical with universe polymorphism and primitive projectionGaëtan Gilbert
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2018-03-28[api] Deprecate a couple of aliases that we missed.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2017-11-28Adding a variant get_truncation_family_of of get_sort_family_of.Hugo Herbelin
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-07-27deprecate Pp.std_ppcmds type aliasMatej Košík
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-02-14Definining EConstr-based contexts.Pierre-Marie Pédrot
2017-02-14Removing compatibility layers in RetypingPierre-Marie Pédrot
2017-02-14Cleaning up opening of the EConstr module in pretyping folder.Pierre-Marie Pédrot
2017-02-14Making judgment type generic over the type of inner constrs.Pierre-Marie Pédrot
2017-02-14Retyping API using EConstr.Pierre-Marie Pédrot
2016-10-07Fix bug #4464: "Anomaly: variable H' unbound. Please report.".Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2015-01-12Update headers.Maxime Dénès
2014-09-18Fix constrMatching as well as change/e_contextually to allowMatthieu Sozeau
2014-06-01Use of "H"-based names for propositional hypotheses obtained byHugo Herbelin
2014-05-06Initial work on reintroducing old-style polymorphism for compatibility (the s...Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-23Removing dead code, thanks to new OCaml warnings and a bit of scripting.Pierre-Marie Pédrot
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2013-03-17Retyping.get_type_of: a lax version raising no anomaliesletouzey
2012-08-08Updating headers.herbelin
2011-07-04Extraction: forbid Prop-polymorphism of inductives when extracting to Ocamlletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-05-23A try at using sort variables during unification. Instead of refreshingmsozeau
2009-04-08- Fixing bug #2084 (unification not checking sort constraints), hopingherbelin
2008-10-18Optimisation de clenv.ml pour que meta_instance ne soit pas appeléherbelin
2008-10-07fixing r11433 again:barras
2006-10-29Compatibilité du polymorphisme de constantes avec les sections.herbelin
2006-10-28Extension du polymorphisme de sorte au cas des définitions dans Type.herbelin
2006-05-28- Indtypes: en attente opinion CoRN, les occurrences de Type non explicitesherbelin
2006-03-29Inductifs avec polymorphisme de sorte (version initiale)herbelin
2004-09-15hiding the meta_map in evar_defsbarras
2004-07-16Nouvelle en-têteherbelin
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
2001-11-06Suppression des local_constraints, des ctxtty et du focus.clrenard
2001-09-19Nouvelle fonction get_sort_family_of pour calculer la famille dans lequel vit...herbelin
2001-03-15entetesfilliatr
2000-12-12syntaxe AST Inversion + commentaires ocamlweb autour de $filliatr
2000-10-18Simplifications autour de typed_type (renommé types par analogie avec sorts)...herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:20:37 +0000