aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/retyping.mli
Commit message (Expand)AuthorAge
* [api] Deprecate a couple of aliases that we missed.Gravatar Emilio Jesus Gallego Arias2018-03-28
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Adding a variant get_truncation_family_of of get_sort_family_of.Gravatar Hugo Herbelin2017-11-28
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
* Removing compatibility layers in RetypingGravatar Pierre-Marie Pédrot2017-02-14
* Cleaning up opening of the EConstr module in pretyping folder.Gravatar Pierre-Marie Pédrot2017-02-14
* Making judgment type generic over the type of inner constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Retyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Fix bug #4464: "Anomaly: variable H' unbound. Please report.".Gravatar Pierre-Marie Pédrot2016-10-07
* 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
* Fix constrMatching as well as change/e_contextually to allowGravatar Matthieu Sozeau2014-09-18
* Use of "H"-based names for propositional hypotheses obtained byGravatar Hugo Herbelin2014-06-01
* Initial work on reintroducing old-style polymorphism for compatibility (the s...Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* 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
* Retyping.get_type_of: a lax version raising no anomaliesGravatar letouzey2013-03-17
* Updating headers.Gravatar herbelin2012-08-08
* Extraction: forbid Prop-polymorphism of inductives when extracting to OcamlGravatar letouzey2011-07-04
* 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
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* A try at using sort variables during unification. Instead of refreshingGravatar msozeau2009-05-23
* - Fixing bug #2084 (unification not checking sort constraints), hopingGravatar herbelin2009-04-08
* Optimisation de clenv.ml pour que meta_instance ne soit pas appeléGravatar herbelin2008-10-18
* fixing r11433 again:Gravatar barras2008-10-07
* Compatibilité du polymorphisme de constantes avec les sections.Gravatar herbelin2006-10-29
* Extension du polymorphisme de sorte au cas des définitions dans Type.Gravatar herbelin2006-10-28
* - Indtypes: en attente opinion CoRN, les occurrences de Type non explicitesGravatar herbelin2006-05-28
* Inductifs avec polymorphisme de sorte (version initiale)Gravatar herbelin2006-03-29
* hiding the meta_map in evar_defsGravatar barras2004-09-15
* Nouvelle en-têteGravatar herbelin2004-07-16
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
* Suppression des local_constraints, des ctxtty et du focus.Gravatar clrenard2001-11-06
* Nouvelle fonction get_sort_family_of pour calculer la famille dans lequel vit...Gravatar herbelin2001-09-19
* 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
* Renommage mk_unsafe_judgment en get_judgment_of; ajout get_assumption_ofGravatar herbelin2000-06-29
* Ajout du langage de tactiquesGravatar delahaye2000-05-03
* documentationGravatar filliatr2000-01-28
* Nouveaux types 'constructor' et 'inductive' dans Term;Gravatar herbelin1999-12-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-06 11:05:10 +0000