aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
2011-11-21Typoherbelin
2011-10-26When checking for emptiness, use Foo.is_empty instead of (=) Foo.emptyletouzey
2011-10-26Environ.set_universes is dead codeletouzey
2011-10-26Mod_subst: some simplifications, some more significant names to functions, etcletouzey
2011-10-25First attempt at making Print Assumption compatible with opaque modules (fix ...letouzey
2011-10-24Mod_subst: Attempt to fix #2608letouzey
2011-10-11Safe_typing: adding a inductive block adds many labels (fix #2603)letouzey
2011-10-11Names : check of labels, cleanup, nicer debug display of kn and constantletouzey
2011-10-11Mod_subst: an unused functionletouzey
2011-10-11More on r14536 (an unused pattern-matching remained in the commit).herbelin
2011-10-11Various simplifications about constant_of_delta and mind_of_deltaletouzey
2011-10-10Hash-consing of mutual_inductive_body (and Univ.constraints)letouzey
2011-10-10Avoid some re-allocation during hash-cons of dir_pathletouzey
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-08Rely on kernel to know if a name is already used so as to be consistent with it.herbelin
2011-10-05Fixing critical inductive polymorphism bug found by Bruno.herbelin
2011-10-05It happens that the type inference algorithm (pretyping) did not checkherbelin
2011-10-02Hash-consing of constr could share moreletouzey
2011-09-25Polishing commits r14492, r14448 and r14407 (tactics propagateherbelin
2011-09-24Completing r14448 and thus continuing r14407 (using Cast to 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-15Names.make_mbid and co : convert from/to identifier (avoid some String.copy)letouzey
2011-09-08More twicks on hash-consingletouzey
2011-09-07Fix the hconsing of universesletouzey
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-08-01fixed bug 2580. Quick fix: copy emitcodes before patching itbarras
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-29Environ: generic equality on named_context replaced by named_context_equalpuech
2011-07-29Term: added function eq_named_declarationpuech
2011-07-29Indtypes: remove useless and wrong generic equality test on constr arraypuech
2011-07-29Term: slight reorganization of the filepuech
2011-07-29Term_typing, Typeops: replace some generic '=' on constr by eq_constrpuech
2011-07-29Term: Refactoring of hashconsingpuech
2011-07-29argument renaming in liftn (match with usual terminology)puech
2011-07-04Extraction: forbid Prop-polymorphism of inductives when extracting to Ocamlletouzey
2011-05-17Modops: the strengthening functions can work without any env argumentletouzey
2011-05-11Print Module (Type) M now tries to print more detailsletouzey
2011-04-19Fix thumb2-related build errorglondu
2011-04-13Revert "Add [Polymorphic] flag for defs"msozeau
2011-04-13- Remove create_evar_defsmsozeau
2011-04-13Fix merge.msozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:22:47 +0000