index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
inductiveops.mli
Commit message (
Expand
)
Author
Age
*
Retyping API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Reductionops API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Disallow dependent case on prim records w/o eta
Matthieu Sozeau
2016-07-06
*
Renaming to more generic has_dependent_elim test
Matthieu Sozeau
2016-07-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
*
|
CLEANUP: kernel/context.ml{,i}
Matej Kosik
2016-01-11
*
|
An example in centralizing similar functions to a common place so that
Hugo Herbelin
2015-12-05
|
/
*
Fix handling of primitive projections in VM.
Maxime Dénès
2015-07-05
*
Fully fixing bug #3491 (anomaly when building _rect scheme in the
Hugo Herbelin
2015-03-25
*
Update headers.
Maxime Dénès
2015-01-12
*
Change the way primitive projections are declared to the kernel.
Matthieu Sozeau
2014-08-28
*
Fix non-printing of coercions for primitive projections (fixes bug #3433).
Matthieu Sozeau
2014-08-14
*
A new step in the new "standard" naming policy for propositional hypotheses
Hugo Herbelin
2014-08-05
*
Move to a representation of universe polymorphic constants using indices for ...
Matthieu Sozeau
2014-08-03
*
Continuing (incomplete) cleaning of Inductiveops.
Hugo Herbelin
2014-08-01
*
A tentative uniform naming policy in module Inductiveops.
Hugo Herbelin
2014-08-01
*
Use of "H"-based names for propositional hypotheses obtained by
Hugo Herbelin
2014-06-01
*
Dead code + typo.
Hugo Herbelin
2014-05-31
*
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
*
Merging Context and Sign.
ppedrot
2013-04-29
*
Splitting Term into five unrelated interfaces:
ppedrot
2013-04-29
*
Updating headers.
herbelin
2012-08-08
*
"Let in" in pattern hell, one more iteration
pboutill
2012-03-02
*
Inductiveops.nb_*{,_env} cleaning
pboutill
2012-01-16
*
Granted legitimate wish #2607 (not exposing crude fixpoint body of
herbelin
2011-12-18
*
A few extra combinators about rel_declaration/named_declaration + a bit of doc
herbelin
2011-04-06
*
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
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
- Inductive types in the "using" option of auto/eauto/firstorder are
herbelin
2009-09-13
*
Ensures that let-in's in arities of inductive types work well. Maybe not
herbelin
2009-08-11
*
- Fixing bug #2139 (kernel-based test of well-formation of elimination
herbelin
2009-07-15
*
Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->
herbelin
2008-12-31
*
fixing r11433 again:
barras
2008-10-07
*
Correction d'une incohérence de typage des inductifs polymorphes: les
herbelin
2008-07-25
*
Suppression argument pattern_source du case_info (code jamais utilisé)
herbelin
2007-03-15
*
Ajout allowed_sorts
herbelin
2006-10-01
*
Nouvelle implantation du polymorphisme de sorte pour les familles inductives
herbelin
2006-05-23
*
- Distinction explicite des parties paramètres et arguments dans le type
herbelin
2006-04-27
*
Fonctions retournant les arits des constructeurs et inductifs
herbelin
2006-01-30
*
Moving subst_inductive from tacinterp to inductiveops for better for reuse in...
herbelin
2005-02-18
*
Compatibilité ocamlweb pour cible doc
herbelin
2005-01-21
*
Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changed
sacerdot
2005-01-14
*
Deplacement des fonctions de typage des predicate de Cases a la V7 de inducti...
herbelin
2004-08-24
*
Nouvelle en-tête
herbelin
2004-07-16
[next]