aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/term.ml
Commit message (Expand)AuthorAge
* 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
* TypoGravatar herbelin2011-11-21
* More on r14536 (an unused pattern-matching remained in the commit).Gravatar herbelin2011-10-11
* Hash-cons the statically allocated Rels (1 to 16) to themselvesGravatar letouzey2011-10-10
* Hash-cons of constr : avoid some useless allocationsGravatar letouzey2011-10-10
* Hash-consing of constr could share moreGravatar letouzey2011-10-02
* Polishing commits r14492, r14448 and r14407 (tactics propagateGravatar herbelin2011-09-25
* Remove specific hash-consing of Term.types (was unused anyway)Gravatar letouzey2011-09-22
* Hash-consing: attempt to stop hash-consing separately constr in declare.mlGravatar letouzey2011-09-22
* More twicks on hash-consingGravatar letouzey2011-09-08
* Having added a special Cast for remembering the use of conversionGravatar herbelin2011-09-04
* Propagated information from the reduction tactics to the kernel soGravatar herbelin2011-08-10
* Term: fix hash_constr to hash modulo casts & names (like compare_constr)Gravatar puech2011-08-08
* Esubst: make types of substitutions & lifts privateGravatar puech2011-08-08
* Term: simplify compare_constr by removing calls to decompose_appGravatar puech2011-08-01
* 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
* Hahtbl_alt: separate generic combine functionsGravatar puech2011-07-29
* Term: added function eq_named_declarationGravatar puech2011-07-29
* Term: slight reorganization of the fileGravatar puech2011-07-29
* Term: Refactoring of hashconsingGravatar puech2011-07-29