index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
indrec.mli
Commit message (
Expand
)
Author
Age
*
Update headers following #6543.
Théo Zimmermann
2018-02-27
*
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-11-06
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
Remove the Sigma (monotonous state) API.
Maxime Dénès
2017-06-06
*
Move is_prim... to Inductiveops and correct Scheme
Matthieu Sozeau
2016-07-06
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
Removing some goal unsafeness in inductive schemes.
Pierre-Marie Pédrot
2015-10-29
|
/
*
Update headers.
Maxime Dénès
2015-01-12
*
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
*
Modulification of identifier
ppedrot
2012-12-14
*
Updating headers.
herbelin
2012-08-08
*
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
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Move from ocamlweb to ocamdoc to generate mli documentation
pboutill
2010-04-29
*
Restructuration of command.ml + generic infrastructure for inductive schemes
herbelin
2009-11-08
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
- Fixed bug 1968 (inversion failing due to a Not_found bug introduced in
herbelin
2008-11-09
*
Nettoyage et standardisation des messages d'erreurs.
herbelin
2007-05-17
*
Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...
herbelin
2005-12-17
*
Types inductifs parametriques
mohring
2005-11-02
*
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
*
Ajout construction If primitive dans constr_expr et rawconstr
herbelin
2003-09-09
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29
*
- Reforme de la gestion des args recursifs (via arbres reguliers)
barras
2002-02-14
*
Suppression des local_constraints, des ctxtty et du focus.
clrenard
2001-11-06
*
GROS COMMIT:
barras
2001-11-05