aboutsummaryrefslogtreecommitdiff
path: root/pretyping/retyping.ml
AgeCommit message (Expand)Author
2014-10-02Work around issues with FO unification trying to unify terms ofMatthieu Sozeau
2014-10-01Fixing use of arguments renaming in apply which was broken afterHugo Herbelin
2014-09-27Make pattern_of_constr typed so that we can infer the proper patternsMatthieu Sozeau
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
2014-09-18Fix constrMatching as well as change/e_contextually to allowMatthieu Sozeau
2014-09-18Fix debug printing with primitive projections.Matthieu Sozeau
2014-06-28Quickly fixing bug #2996: typing functions now check when referring toHugo Herbelin
2014-06-17Removing dead code.Pierre-Marie Pédrot
2014-06-01Use of "H"-based names for propositional hypotheses obtained byHugo Herbelin
2014-05-06- Fix arity handling in retyping (de Bruijn bug!)Matthieu Sozeau
2014-05-06Allow records whose sort is defined by a constant.Matthieu Sozeau
2014-05-06Fix interface for template polymorphism, cleaning up code in all typing algor...Matthieu Sozeau
2014-05-06Properly reinstate old-style polymorphism in the kernel and pretyping/retyping.Matthieu Sozeau
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
2013-09-19Get rid of the uses of deprecated OCaml elements (still remaining compatible ...xclerc
2013-07-19- Fix uncaught exception NotASort from reductionops, moving decomp_sort to re...msozeau
2013-05-14Delayed the computation of parameters in sort polymorphism ofherbelin
2013-05-05Hack to solve a "Bad recursive type" anomaly.herbelin
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-03-17Retyping.get_type_of: a lax version raising no anomaliesletouzey
2013-02-05Fixed bug #2981 (anomaly NotASort in Retyping due to collision betweenherbelin
2013-01-28Uniformization of the "anomaly" command.ppedrot
2012-12-14Modulification of identifierppedrot
2012-11-22Monomorphization (pretyping)ppedrot
2012-09-14Partial revert of Yann commit in order to use CLib.List when openingppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-08-08Updating headers.herbelin
2012-03-02Noise for nothingpboutill
2011-07-04Extraction: forbid Prop-polymorphism of inductives when extracting to Ocamlletouzey
2011-04-11Catch NotArity exception and transform it into an anomaly in retyping.msozeau
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
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
2009-03-04Backtrack sur la mémoïsation de nf_evar.aspiwack
2009-02-27=?utf-8?q?Tentative=20d'optimisation=20(en=20temps)=20sur=20[nf=5Fevar]=20et=...aspiwack
2009-02-06pushed evar reduction in kernelbarras
2009-01-12Fix a bunch of bugs related to setoid_rewrite, unification and evars:msozeau
2008-12-28- Another bug in get_sort_family_of (sort-polymorphism of constants andherbelin
2008-12-26- Extracted from the tactic "now" an experimental tactic "easy" for smallherbelin
2008-10-07fixing r11433 again:barras
2008-06-09- Documentation de admit et Print Assumptions.herbelin
2008-04-27Correction du bug des types singletons pas sous-type de Setherbelin
2008-03-15Application de refresh_universes dans typing.ml et retyping.ml : lesherbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 11:27:13 +0000