aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/term.ml
Commit message (Expand)AuthorAge
* CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | mergeGravatar Matej Kosik2016-01-11
|\ \
| * | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
* | | Remove some unused functions.Gravatar Guillaume Melquiond2016-01-02
|/ /
* | Unifying betazeta_applist and prod_applist into a clearer interface.Gravatar Hugo Herbelin2015-12-05
* | Moving three related small half-general half-ad-hoc utility functionsGravatar Hugo Herbelin2015-12-05
|/
* Adding a function to mirror decompose_prod_n_assum in that it counts let-ins,Gravatar Hugo Herbelin2015-10-18
* Update headers.Gravatar Maxime Dénès2015-01-12
* Revert "Term: include a function to print terms"Gravatar Enrico Tassi2014-12-27
* Term: include a function to print termsGravatar Enrico Tassi2014-12-26
* A patch for printing "match" when constructors are defined with let-inGravatar Hugo Herbelin2014-10-20
* Simplify evarconv thanks to new delta status of projections,Gravatar Matthieu Sozeau2014-09-30
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
* Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...Gravatar Matthieu Sozeau2014-06-10
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Adding a field ci_cstr_nargs to case_info and mind_consnrealargs toGravatar Hugo Herbelin2014-04-28
* Do not generate useless argument arrays in whd_* functions.Gravatar ppedrot2013-10-29
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ...Gravatar xclerc2013-09-19
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* Removing two Pervasives.compare from Term.Gravatar ppedrot2013-04-03
* Term.dest* functions now raise specific DestKO exn instead of Invalid_argumentGravatar letouzey2013-03-12
* More monomorphization.Gravatar ppedrot2013-03-05
* avoid (Int.equal (cmp ...) 0) when a boolean equality existsGravatar letouzey2013-02-19
* Names: revised representation of constants and mutual_inductiveGravatar letouzey2013-02-19
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
* * Kernel/Terms:Gravatar regisgia2013-01-06
* Modulification of nameGravatar ppedrot2012-12-18
* Modulification of identifierGravatar ppedrot2012-12-14
* Renamed Option.Misc.compare to the more uniform Option.equal.Gravatar ppedrot2012-12-13
* Fixing a comment.Gravatar herbelin2012-12-04
* Removed some FIXME related to equality on universes.Gravatar ppedrot2012-11-26
* Monomorphization (kernel)Gravatar ppedrot2012-11-22
* More monomorphizationsGravatar ppedrot2012-11-13
* Monomorphized a lot of equalities over OCaml integers, thanks toGravatar ppedrot2012-11-08
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* Reusing the Hashset data structure in Hashcons. Hopefully, this shouldGravatar ppedrot2012-09-26
* Cleaning, renaming obscure functions and documenting in Hashcons.Gravatar ppedrot2012-09-26
* As r15801: putting everything from Util.array_* to CArray.*.Gravatar ppedrot2012-09-14
* kernel/Term:Gravatar regisgia2012-09-14
* The new ocaml compiler (4.00) has a lot of very cool warnings,Gravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* Fixing bug #2817 (occur check was not done up to instantiation ofGravatar herbelin2012-06-20
* Reorganizing the structure of evarutil.ml (only restructuration, noGravatar herbelin2012-03-20
* Noise for nothingGravatar pboutill2012-03-02
* Term: properly ignore Casts between Apps in constr_ordGravatar puech2011-11-29
* Term: useless conversion to list in constr_ord deletedGravatar puech2011-11-29
* Term: Fix hash_constr behavior for Cast lnterleaved in application spines.Gravatar puech2011-11-28