index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
/
term.ml
Commit message (
Expand
)
Author
Age
*
[api] Remove deprecated object from `Term`
Emilio Jesus Gallego Arias
2018-05-30
*
[api] Deprecate a couple of aliases that we missed.
Emilio Jesus Gallego Arias
2018-03-28
*
Update headers following #6543.
Théo Zimmermann
2018-02-27
*
Merge PR #1082: Fixing Print for inductive types with let-in in parameters
Maxime Dénès
2018-02-12
|
\
*
|
Safer VM interfaces
Maxime Dénès
2018-01-26
|
*
Fixes incorrect anomaly message in lambda/prod_applist_assum + typo in doc.
Hugo Herbelin
2017-12-14
|
/
*
[api] Remove aliases of `Evar.t`
Emilio Jesus Gallego Arias
2017-11-26
*
[api] Deprecate Term destructors, move to Constr
Emilio Jesus Gallego Arias
2017-11-22
*
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-11-06
*
[api] Deprecate all legacy uses of Names in core.
Emilio Jesus Gallego Arias
2017-11-06
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
Remove (useless) aliases from the API.
Matej Košík
2017-06-10
*
Drop '.' from CErrors.anomaly, insert it in args
Jason Gross
2017-06-02
*
[cleanup] Unify all calls to the error function.
Emilio Jesus Gallego Arias
2017-05-27
*
More consistent writing of de Bruijn.
Théo Zimmermann
2017-05-01
*
Fix for bug 5507. Mispelt de Bruijn.
Théo Zimmermann
2017-05-01
*
Make the Constr.kind_of_term type parametric in sorts and universes.
Pierre-Marie Pédrot
2017-03-31
*
Reductionops now return EConstrs.
Pierre-Marie Pédrot
2017-02-14
*
Moving unused code out of the kernel into Termops.
Pierre-Marie Pédrot
2016-10-31
*
Make the user_err header an optional parameter.
Emilio Jesus Gallego Arias
2016-08-19
*
Remove errorlabstrm in favor of user_err
Emilio Jesus Gallego Arias
2016-08-19
*
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
CLEANUP: Context.{Rel,Named}.Declaration.t
Matej Kosik
2016-02-09
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
merge
Matej Kosik
2016-01-11
|
\
\
|
*
|
CLEANUP: kernel/context.ml{,i}
Matej Kosik
2016-01-11
*
|
|
Remove some unused functions.
Guillaume Melquiond
2016-01-02
|
/
/
*
|
Unifying betazeta_applist and prod_applist into a clearer interface.
Hugo Herbelin
2015-12-05
*
|
Moving three related small half-general half-ad-hoc utility functions
Hugo Herbelin
2015-12-05
|
/
*
Adding a function to mirror decompose_prod_n_assum in that it counts let-ins,
Hugo Herbelin
2015-10-18
*
Update headers.
Maxime Dénès
2015-01-12
*
Revert "Term: include a function to print terms"
Enrico Tassi
2014-12-27
*
Term: include a function to print terms
Enrico Tassi
2014-12-26
*
A patch for printing "match" when constructors are defined with let-in
Hugo Herbelin
2014-10-20
*
Simplify evarconv thanks to new delta status of projections,
Matthieu Sozeau
2014-09-30
*
Add a boolean to indicate the unfolding state of a primitive projection,
Matthieu Sozeau
2014-09-27
*
Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...
Matthieu Sozeau
2014-06-10
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Adding a field ci_cstr_nargs to case_info and mind_consnrealargs to
Hugo Herbelin
2014-04-28
*
Do not generate useless argument arrays in whd_* functions.
ppedrot
2013-10-29
*
Get rid of the uses of deprecated OCaml elements (still remaining compatible ...
xclerc
2013-09-19
*
Splitting Term into five unrelated interfaces:
ppedrot
2013-04-29
*
Removing two Pervasives.compare from Term.
ppedrot
2013-04-03
*
Term.dest* functions now raise specific DestKO exn instead of Invalid_argument
letouzey
2013-03-12
*
More monomorphization.
ppedrot
2013-03-05
*
avoid (Int.equal (cmp ...) 0) when a boolean equality exists
letouzey
2013-02-19
*
Names: revised representation of constants and mutual_inductive
letouzey
2013-02-19
*
Uniformization of the "anomaly" command.
ppedrot
2013-01-28
*
New implementation of the conversion test, using normalization by evaluation to
mdenes
2013-01-22
[next]