index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
retyping.ml
Commit message (
Expand
)
Author
Age
*
Make pattern_of_constr typed so that we can infer the proper patterns
Matthieu Sozeau
2014-09-27
*
Add a boolean to indicate the unfolding state of a primitive projection,
Matthieu Sozeau
2014-09-27
*
Fix constrMatching as well as change/e_contextually to allow
Matthieu Sozeau
2014-09-18
*
Fix debug printing with primitive projections.
Matthieu Sozeau
2014-09-18
*
Quickly fixing bug #2996: typing functions now check when referring to
Hugo Herbelin
2014-06-28
*
Removing dead code.
Pierre-Marie Pédrot
2014-06-17
*
Use of "H"-based names for propositional hypotheses obtained by
Hugo Herbelin
2014-06-01
*
- Fix arity handling in retyping (de Bruijn bug!)
Matthieu Sozeau
2014-05-06
*
Allow records whose sort is defined by a constant.
Matthieu Sozeau
2014-05-06
*
Fix interface for template polymorphism, cleaning up code in all typing algor...
Matthieu Sozeau
2014-05-06
*
Properly reinstate old-style polymorphism in the kernel and pretyping/retyping.
Matthieu Sozeau
2014-05-06
*
Initial work on reintroducing old-style polymorphism for compatibility (the s...
Matthieu Sozeau
2014-05-06
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Removing dead code, thanks to new OCaml warnings and a bit of scripting.
Pierre-Marie Pédrot
2014-04-23
*
Get rid of the uses of deprecated OCaml elements (still remaining compatible ...
xclerc
2013-09-19
*
- Fix uncaught exception NotASort from reductionops, moving decomp_sort to re...
msozeau
2013-07-19
*
Delayed the computation of parameters in sort polymorphism of
herbelin
2013-05-14
*
Hack to solve a "Bad recursive type" anomaly.
herbelin
2013-05-05
*
Splitting Term into five unrelated interfaces:
ppedrot
2013-04-29
*
Retyping.get_type_of: a lax version raising no anomalies
letouzey
2013-03-17
*
Fixed bug #2981 (anomaly NotASort in Retyping due to collision between
herbelin
2013-02-05
*
Uniformization of the "anomaly" command.
ppedrot
2013-01-28
*
Modulification of identifier
ppedrot
2012-12-14
*
Monomorphization (pretyping)
ppedrot
2012-11-22
*
Partial revert of Yann commit in order to use CLib.List when opening
ppedrot
2012-09-14
*
This patch removes unused "open" (automatically generated from
regisgia
2012-09-14
*
Updating headers.
herbelin
2012-08-08
*
Noise for nothing
pboutill
2012-03-02
*
Extraction: forbid Prop-polymorphism of inductives when extracting to Ocaml
letouzey
2011-07-04
*
Catch NotArity exception and transform it into an anomaly in retyping.
msozeau
2011-04-11
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
A try at using sort variables during unification. Instead of refreshing
msozeau
2009-05-23
*
- Fixing bug #2084 (unification not checking sort constraints), hoping
herbelin
2009-04-08
*
Backtrack sur la mémoïsation de nf_evar.
aspiwack
2009-03-04
*
=?utf-8?q?Tentative=20d'optimisation=20(en=20temps)=20sur=20[nf=5Fevar]=20et=...
aspiwack
2009-02-27
*
pushed evar reduction in kernel
barras
2009-02-06
*
Fix a bunch of bugs related to setoid_rewrite, unification and evars:
msozeau
2009-01-12
*
- Another bug in get_sort_family_of (sort-polymorphism of constants and
herbelin
2008-12-28
*
- Extracted from the tactic "now" an experimental tactic "easy" for small
herbelin
2008-12-26
*
fixing r11433 again:
barras
2008-10-07
*
- Documentation de admit et Print Assumptions.
herbelin
2008-06-09
*
Correction du bug des types singletons pas sous-type de Set
herbelin
2008-04-27
*
Application de refresh_universes dans typing.ml et retyping.ml : les
herbelin
2008-03-15
*
Compatibilité du polymorphisme de constantes avec les sections.
herbelin
2006-10-29
*
Extension du polymorphisme de sorte au cas des définitions dans Type.
herbelin
2006-10-28
*
- Indtypes: en attente opinion CoRN, les occurrences de Type non explicites
herbelin
2006-05-28
*
Nouvelle implantation du polymorphisme de sorte pour les familles inductives
herbelin
2006-05-23
*
Inductifs avec polymorphisme de sorte (version initiale)
herbelin
2006-03-29
[next]