aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Suppression quotifyGravatar herbelin2004-07-16
* Suppression compilation explication.ml4Gravatar herbelin2004-07-16
* Abstraction vis a vis de dummy_locGravatar herbelin2004-07-16
* Branchement sur Util.loc et abstraction vis a vis de dummy_locGravatar herbelin2004-07-16
* Suppression de Rawterm.loc, branchement sur Util.locGravatar herbelin2004-07-16
* Abstraction vis a vis de dummy_locGravatar herbelin2004-07-16
* majGravatar filliatr2004-07-15
* majGravatar filliatr2004-07-14
* ajout des unsafeCoerce + 2 bugs haskellGravatar letouzey2004-07-14
* majGravatar filliatr2004-07-13
* bug #780: compilation of several units in the same coqtop processGravatar barras2004-07-13
* bug #794: conv made in wrong envGravatar barras2004-07-13
* bug #790: better error_not_cleanGravatar barras2004-07-13
* bugs #667 and #783 (mimick_evar and loc_table on large files)Gravatar barras2004-07-13
* majGravatar filliatr2004-07-12
* MAJ techniqueGravatar herbelin2004-07-12
* majGravatar filliatr2004-07-11
* Eta-expansion du predicat dans build_indrec (suite)Gravatar herbelin2004-07-11
* Eta-expansion du predicat pas seulement pour make_case mais aussi pour build_...Gravatar herbelin2004-07-11
* Backtrack sur l'eta-expansion systematique et incorrect du predicat du Cases ...Gravatar herbelin2004-07-11
* majGravatar filliatr2004-07-09
* majGravatar filliatr2004-07-08
* majGravatar filliatr2004-07-08
* * <style>...</style> tag no longer generated for theory filesGravatar sacerdot2004-07-08
* - recent changes to doubleTypeInference.ml (that introduced doubleGravatar sacerdot2004-07-08
* Commit to perform double type inference also on inner types.Gravatar sacerdot2004-07-08
* added commands to ideGravatar corbinea2004-07-08
* majGravatar filliatr2004-07-07
* bypass w_Define when w_refine-ingGravatar corbinea2004-07-07
* majGravatar filliatr2004-07-06
* majGravatar filliatr2004-07-05
* Constants just after a "Let id : t. ... Qed" local variable declaration wereGravatar sacerdot2004-07-05
* majGravatar filliatr2004-07-04
* majGravatar filliatr2004-07-02
* syntax compatibility fixGravatar corbinea2004-07-02
* majGravatar filliatr2004-07-01
* majGravatar filliatr2004-06-30
* majGravatar filliatr2004-06-30
* updated printing of evar context (may loop ?)Gravatar corbinea2004-06-30
* instantiate entry: constr -> lconstrGravatar corbinea2004-06-30
* majGravatar filliatr2004-06-29
* majGravatar filliatr2004-06-29
* Essai de suppression de eta dans simpl (cf bug #779)Gravatar herbelin2004-06-29
* moved instantiate binding to extratacticsGravatar corbinea2004-06-29
* License de contrib/interfaceGravatar herbelin2004-06-29
* efficacite du lexeurGravatar filliatr2004-06-29
* majGravatar filliatr2004-06-28
* majGravatar filliatr2004-06-28
* contrib/interface *$*$@!Gravatar corbinea2004-06-28
* more evar stuffGravatar corbinea2004-06-28
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 07:16:37 +0000