aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
* Proof using ...Gravatar gareuselesinge2011-12-12
* 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
* When checking for emptiness, use Foo.is_empty instead of (=) Foo.emptyGravatar letouzey2011-10-26
* Environ.set_universes is dead codeGravatar letouzey2011-10-26
* Mod_subst: some simplifications, some more significant names to functions, etcGravatar letouzey2011-10-26
* First attempt at making Print Assumption compatible with opaque modules (fix ...Gravatar letouzey2011-10-25
* Mod_subst: Attempt to fix #2608Gravatar letouzey2011-10-24
* Safe_typing: adding a inductive block adds many labels (fix #2603)Gravatar letouzey2011-10-11
* Names : check of labels, cleanup, nicer debug display of kn and constantGravatar letouzey2011-10-11
* Mod_subst: an unused functionGravatar letouzey2011-10-11
* More on r14536 (an unused pattern-matching remained in the commit).Gravatar herbelin2011-10-11
* Various simplifications about constant_of_delta and mind_of_deltaGravatar letouzey2011-10-11
* Hash-consing of mutual_inductive_body (and Univ.constraints)Gravatar letouzey2011-10-10
* Avoid some re-allocation during hash-cons of dir_pathGravatar letouzey2011-10-10
* 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
* Rely on kernel to know if a name is already used so as to be consistent with it.Gravatar herbelin2011-10-08
* Fixing critical inductive polymorphism bug found by Bruno.Gravatar herbelin2011-10-05
* It happens that the type inference algorithm (pretyping) did not checkGravatar herbelin2011-10-05
* Hash-consing of constr could share moreGravatar letouzey2011-10-02
* Polishing commits r14492, r14448 and r14407 (tactics propagateGravatar herbelin2011-09-25
* Completing r14448 and thus continuing r14407 (using Cast to propagateGravatar herbelin2011-09-24
* 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
* Names.make_mbid and co : convert from/to identifier (avoid some String.copy)Gravatar letouzey2011-09-15
* More twicks on hash-consingGravatar letouzey2011-09-08
* Fix the hconsing of universesGravatar letouzey2011-09-07
* 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
* fixed bug 2580. Quick fix: copy emitcodes before patching itGravatar barras2011-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
* Environ: generic equality on named_context replaced by named_context_equalGravatar puech2011-07-29
* Term: added function eq_named_declarationGravatar puech2011-07-29
* Indtypes: remove useless and wrong generic equality test on constr arrayGravatar puech2011-07-29
* Term: slight reorganization of the fileGravatar puech2011-07-29
* Term_typing, Typeops: replace some generic '=' on constr by eq_constrGravatar puech2011-07-29
* Term: Refactoring of hashconsingGravatar puech2011-07-29
* argument renaming in liftn (match with usual terminology)Gravatar puech2011-07-29
* Extraction: forbid Prop-polymorphism of inductives when extracting to OcamlGravatar letouzey2011-07-04
* Modops: the strengthening functions can work without any env argumentGravatar letouzey2011-05-17
* Print Module (Type) M now tries to print more detailsGravatar letouzey2011-05-11