aboutsummaryrefslogtreecommitdiff
path: root/kernel/term.ml
AgeCommit message (Expand)Author
2012-12-18Modulification of nameppedrot
2012-12-14Modulification of identifierppedrot
2012-12-13Renamed Option.Misc.compare to the more uniform Option.equal.ppedrot
2012-12-04Fixing a comment.herbelin
2012-11-26Removed some FIXME related to equality on universes.ppedrot
2012-11-22Monomorphization (kernel)ppedrot
2012-11-13More monomorphizationsppedrot
2012-11-08Monomorphized a lot of equalities over OCaml integers, thanks toppedrot
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-09-26Reusing the Hashset data structure in Hashcons. Hopefully, this shouldppedrot
2012-09-26Cleaning, renaming obscure functions and documenting in Hashcons.ppedrot
2012-09-14As r15801: putting everything from Util.array_* to CArray.*.ppedrot
2012-09-14kernel/Term:regisgia
2012-09-14The new ocaml compiler (4.00) has a lot of very cool warnings,regisgia
2012-08-08Updating headers.herbelin
2012-06-20Fixing bug #2817 (occur check was not done up to instantiation ofherbelin
2012-03-20Reorganizing the structure of evarutil.ml (only restructuration, noherbelin
2012-03-02Noise for nothingpboutill
2011-11-29Term: properly ignore Casts between Apps in constr_ordpuech
2011-11-29Term: useless conversion to list in constr_ord deletedpuech
2011-11-28Term: Fix hash_constr behavior for Cast lnterleaved in application spines.puech
2011-11-21Typoherbelin
2011-10-11More on r14536 (an unused pattern-matching remained in the commit).herbelin
2011-10-10Hash-cons the statically allocated Rels (1 to 16) to themselvesletouzey
2011-10-10Hash-cons of constr : avoid some useless allocationsletouzey
2011-10-02Hash-consing of constr could share moreletouzey
2011-09-25Polishing commits r14492, r14448 and r14407 (tactics propagateherbelin
2011-09-22Remove specific hash-consing of Term.types (was unused anyway)letouzey
2011-09-22Hash-consing: attempt to stop hash-consing separately constr in declare.mlletouzey
2011-09-08More twicks on hash-consingletouzey
2011-09-04Having added a special Cast for remembering the use of conversionherbelin
2011-08-10Propagated information from the reduction tactics to the kernel soherbelin
2011-08-08Term: fix hash_constr to hash modulo casts & names (like compare_constr)puech
2011-08-08Esubst: make types of substitutions & lifts privatepuech
2011-08-01Term: simplify compare_constr by removing calls to decompose_apppuech
2011-07-29Extraction: replace generic = on mutual_inductive_body by mib_equalpuech
2011-07-29Term: moved function constr_ord (a.k.a compare_constr) from Sequent to Termpuech
2011-07-29Ccalgo, Ccproof: multiple generic Hashtbl on constr and term replaced by Cons...puech
2011-07-29Hahtbl_alt: separate generic combine functionspuech
2011-07-29Term: added function eq_named_declarationpuech
2011-07-29Term: slight reorganization of the filepuech
2011-07-29Term: Refactoring of hashconsingpuech
2011-07-29argument renaming in liftn (match with usual terminology)puech
2011-04-06A few extra combinators about rel_declaration/named_declaration + a bit of docherbelin
2010-12-01* Kernel/Term:regisgia
2010-12-01* Kernel/Termregisgia
2010-12-01* Kernel/Termregisgia
2010-11-03Remove suspiciously named "implicit" stuff from Termglondu
2010-10-05Reintroduce kind_of_type (used by Presburger contrib)glondu
2010-09-28Remove kind_of_type, kind_of_term2 (dead code)glondu
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 05:17:36 +0000