index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
classops.mli
Commit message (
Expand
)
Author
Age
*
Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...
Matthieu Sozeau
2016-04-04
|
\
*
|
Update copyright headers.
Maxime Dénès
2016-01-20
|
*
Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080
Jason Gross
2015-08-14
|
/
*
Continuing handling of NoCoercion after df6e64fd28 and 4944b5e72.
Hugo Herbelin
2015-07-10
*
Update headers.
Maxime Dénès
2015-01-12
*
A few Global.env removed.
Hugo Herbelin
2014-10-04
*
Add a boolean to indicate the unfolding state of a primitive projection,
Matthieu Sozeau
2014-09-27
*
Adapt coercion code to work with projections as target classes.
Matthieu Sozeau
2014-06-17
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2014-03-05
*
Restrict (try...with...) to avoid catching critical exn (part 5)
letouzey
2013-03-13
*
Added a Local Definition vernacular command. This type of definition
ppedrot
2013-03-11
*
More equality functions
ppedrot
2012-11-25
*
Updating headers.
herbelin
2012-08-08
*
global_reference migrated from Libnames to new Globnames, less deps in gramma...
letouzey
2012-05-29
*
An automatic substitution of scope at functor application
letouzey
2011-02-11
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
New script dev/tools/change-header to automatically update Coq files headers.
herbelin
2010-06-22
*
Various minor improvements of comments in mli for ocamldoc
letouzey
2010-04-29
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Move from ocamlweb to ocamdoc to generate mli documentation
pboutill
2010-04-29
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Propagating commit 11343 from branch v8.2 to trunk (wish 1934 about
herbelin
2008-09-02
*
Prise en compte des coercions dans les clauses "with" même si le type
herbelin
2008-04-23
*
Moving centralised discharge into dispatched discharge_function; required to ...
herbelin
2005-02-18
*
Names.substitution (and related functions) and Term.subst_mps moved to
sacerdot
2004-11-16
*
Nouvelle en-tête
herbelin
2004-07-16
*
Déplacement de Declare juste à la fin de interp pour pouvoir accéder à in...
herbelin
2003-09-12
*
Tables logarithmiques pour les coercions + nettoyage
herbelin
2003-06-08
*
Intégration des modifs de la branche mowgli :
herbelin
2002-11-05
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29
*
compat ocaml 3.03
filliatr
2001-12-13
*
Mise en place de coercion dans les motifs
herbelin
2001-12-11
*
Nettoyage coercions et classes
herbelin
2001-11-09
*
Suppression des local_constraints, des ctxtty et du focus.
clrenard
2001-11-06
*
GROS COMMIT:
barras
2001-11-05
*
Suppression option immediate_discharge; nettoyage de Declare et conséquences
herbelin
2001-10-11
*
Suppression des arguments sur les constantes, inductifs et constructeurs
barras
2001-10-09
*
Débogage discharge des coercions; nettoyage
herbelin
2001-07-05
*
entetes
filliatr
2001-03-15
*
Ajout d'une commande pour afficher chaque coercion à la demandeparsing/g_bas...
herbelin
2001-02-06
*
Un nom long pour les variables de section qui font classe ou coercion; réorg...
herbelin
2000-12-25
*
syntaxe AST Inversion + commentaires ocamlweb autour de $
filliatr
2000-12-12
*
Utilisation de global_reference dans rawconstr
herbelin
2000-11-20
*
Changement de représentation du contexte des réf dans rawconstr et pattern
herbelin
2000-04-28
*
N'importe quel rawconstr maintenant dans le contexte d'une référence
herbelin
2000-04-26
*
Commentaire
herbelin
2000-03-07
*
erreurs latex dans interfaces
filliatr
2000-01-27
*
Déplacement non-affichage des coercions dans termast
herbelin
2000-01-07
[next]