aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/term.mli
Commit message (Expand)AuthorAge
* Moving unused code out of the kernel into Termops.Gravatar Pierre-Marie Pédrot2016-10-31
* Shrink Proofs/Obligations by default and deprecateGravatar Matthieu Sozeau2016-06-27
* Term: fix a comment (first de Bruijn index is 1)Gravatar Pierre Letouzey2016-02-16
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
* | 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
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-19
|\|
| * Adding a function to mirror decompose_prod_n_assum in that it counts let-ins,Gravatar Hugo Herbelin2015-10-18
* | Splitting kernel universe code in two modules.Gravatar Pierre-Marie Pédrot2015-10-06
|/
* 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
* Fix typo in comment.Gravatar Maxime Dénès2014-03-05
* Do not generate useless argument arrays in whd_* functions.Gravatar ppedrot2013-10-29
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* Checker: regroup all vo-related types in cic.mliGravatar letouzey2013-04-15
* Comments in mliGravatar pboutill2013-03-25
* Restrict (try...with...) to avoid catching critical exn (part 5)Gravatar letouzey2013-03-13
* Term.dest* functions now raise specific DestKO exn instead of Invalid_argumentGravatar letouzey2013-03-12
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
* Modulification of nameGravatar ppedrot2012-12-18
* Modulification of identifierGravatar ppedrot2012-12-14
* Removed some FIXME related to equality on universes.Gravatar ppedrot2012-11-26
* More monomorphizationsGravatar ppedrot2012-11-13
* 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
* Fixing vm_compute bug #2729 (function used to decompose constructorsGravatar herbelin2012-03-13
* More on r14536 (an unused pattern-matching remained in the commit).Gravatar herbelin2011-10-11
* Hash-consing of mutual_inductive_body (and Univ.constraints)Gravatar letouzey2011-10-10
* Hash-consing of constr could share moreGravatar letouzey2011-10-02
* Remove specific hash-consing of Term.types (was unused anyway)Gravatar letouzey2011-09-22
* More twicks on hash-consingGravatar letouzey2011-09-08
* Propagated information from the reduction tactics to the kernel soGravatar herbelin2011-08-10
* Extraction: replace generic = on mutual_inductive_body by mib_equalGravatar puech2011-07-29
* Term: moved function constr_ord (a.k.a compare_constr) from Sequent to TermGravatar puech2011-07-29
* Ccalgo, Ccproof: multiple generic Hashtbl on constr and term replaced by Cons...Gravatar puech2011-07-29
* Term: added function eq_named_declarationGravatar puech2011-07-29
* A few extra combinators about rel_declaration/named_declaration + a bit of docGravatar herbelin2011-04-06
* Fixing bug #2454: inversion predicate strategy for inferring the typeGravatar herbelin2010-12-19
* Remove suspiciously named "implicit" stuff from TermGravatar glondu2010-11-03
* Reintroduce kind_of_type (used by Presburger contrib)Gravatar glondu2010-10-05