aboutsummaryrefslogtreecommitdiff
path: root/pretyping/coercion.mli
AgeCommit message (Expand)Author
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-01-06Fix #11140: Bidirectionality hints perform (surprising?) simplificationMaxime Dénès
2019-11-26coercion functions are never called without a term to coerceGaëtan Gilbert
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-02-08Coercion intf fixMatthieu Sozeau
2019-02-08[evarconv] New flag handling for unifierMatthieu Sozeau
2019-02-05Make Program a regular attributeMaxime Dénès
2018-02-27Update headers following #6543.Théo Zimmermann
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-04-27Remove unused [open] statementsGaetan Gilbert
2017-04-25[location] Remove Loc.ghost.Emilio Jesus Gallego Arias
2017-02-14Making judgment type generic over the type of inner constrs.Pierre-Marie Pédrot
2017-02-14Coercion API using EConstr.Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-10-04A few Global.env removed.Hugo Herbelin
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-02-12TC: honor the use_typeclasses flag in pretypingEnrico Tassi
2013-04-29Merging Context and Sign.ppedrot
2012-08-08Updating headers.herbelin
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-05-29remove many excessive open Util & Errors in mli'sletouzey
2012-03-14Second step of integration of Program:msozeau
2012-03-14Remove support for "abstract typing constraints" that requires unicity of sol...msozeau
2012-03-02Noise for nothingpboutill
2010-12-23Rename rawterm.ml into glob_term.mlglondu
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-11-11Promote evar_defs to evar_map (in Evd)glondu
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2008-06-21Various improvements in handling of evars in general and typingmsozeau
2008-04-23Prise en compte des coercions dans les clauses "with" même si le typeherbelin
2006-05-29The "clean integration of subtac" patch.msozeau
2006-04-07- Documentation of the Program tactics.msozeau
2006-03-22Made pretyping a functor over a coercion implementation. Pretyping.Default us...msozeau
2006-02-08Localisation des erreurs de sorte du prétypageherbelin
2006-01-29Documentationherbelin
2004-09-07deuxieme vague de modifs: evar_defs fonctionnelbarras
2004-07-16Nouvelle en-têteherbelin
2004-07-16Suppression de Rawterm.loc, branchement sur Util.locherbelin
2001-12-11Mise en place de coercion dans les motifsherbelin
2001-11-06Suppression des local_constraints, des ctxtty et du focus.clrenard
2001-09-14L'instantiation des evars quand un produit ou une sorte étaient attendus n'Ã...herbelin
2001-03-15entetesfilliatr
2000-12-12syntaxe AST Inversion + commentaires ocamlweb autour de $filliatr
2000-11-08Insertion de coercion au milieu des applications partielles et propagation de...herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 08:08:10 +0000