aboutsummaryrefslogtreecommitdiff
path: root/interp
AgeCommit message (Expand)Author
2017-09-15Merge PR #1037: Parse directly to Sorts.family when appropriate.Maxime Dénès
2017-09-12Adding a missing period in a notation warning.Hugo Herbelin
2017-09-12Fixing bugs of a67bd7f9 and c6d9d4fb in recognizing a 'pat binding.Hugo Herbelin
2017-09-12Fixing a typo in printing notations with recursive binders.Hugo Herbelin
2017-09-12Fixing a bug of recursive notations introduced in dfdaf4de.Hugo Herbelin
2017-09-12Fixing little inaccuracy in coercions to ident or name.Hugo Herbelin
2017-09-08Parse directly to Sorts.family when appropriate.Gaëtan Gilbert
2017-09-04Making detyping potentially lazy.Pierre-Marie Pédrot
2017-08-31Merge PR #980: Adding combinators + a canonical renaming in List, Option, NameMaxime Dénès
2017-08-29Merge PR #946: Functional pretyping interfaceMaxime Dénès
2017-08-29Merge PR #916: Fixing notation bug 5608 involving { } and a slight restructur...Maxime Dénès
2017-08-29Merge PR #773: [flags] Remove XML output flag.Maxime Dénès
2017-08-29A new step of restructuration of notations.Hugo Herbelin
2017-08-29A little reorganization of notations + a fix to #5608.Hugo Herbelin
2017-08-29Adapting code to renaming Array.fold_map -> Array.fold_left_map.Hugo Herbelin
2017-08-29Adapting code to renaming fold_map/fold_map' into fold_left_map/fold_right_mapHugo Herbelin
2017-08-01[flags] Remove XML output flag.Emilio Jesus Gallego Arias
2017-08-01Remove understand_tcc_evars.Maxime Dénès
2017-08-01Detyping functions are now operating on EConstr.t.Pierre-Marie Pédrot
2017-07-31Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t insteadMaxime Dénès
2017-07-28Merge PR #889: Removing template polymorphism for definitions.Maxime Dénès
2017-07-28Merge PR #888: Stronger kernel typesMaxime Dénès
2017-07-27deprecate Pp.std_ppcmds type aliasMatej Košík
2017-07-26Removing template polymorphism for definitions.Pierre-Marie Pédrot
2017-07-26Merge PR #894: Fixing a little location bug with recursive bindersMaxime Dénès
2017-07-26Further simplication: do not recreate entries for side-effects.Pierre-Marie Pédrot
2017-07-26Remove a horrendous hack in Declare to retrieve exported side-effects.Pierre-Marie Pédrot
2017-07-26More precise type of entries capturing their lack of side-effects.Pierre-Marie Pédrot
2017-07-26More precise type for universe entries.Pierre-Marie Pédrot
2017-07-19[general] Move files to directories matching linking order.Emilio Jesus Gallego Arias
2017-07-18Fixing a little location bug with recursive binders.Hugo Herbelin
2017-07-13Remove the function Global.type_of_global_unsafe.Pierre-Marie Pédrot
2017-07-04Merge branch 'v8.6'Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-15Merge PR#713: Bump year in headers.Maxime Dénès
2017-06-15Merge PR#719: Constrexpr.Numeral without bigintMaxime Dénès
2017-06-15Merge PR#375: DeprecationMaxime Dénès
2017-06-14Merge PR#765: Remove obsolete Show commandsMaxime Dénès
2017-06-14[print] Allow Selective Printing of NotationsEmilio Jesus Gallego Arias
2017-06-14Notation.declare_rawnumeral_interpreterPierre Letouzey
2017-06-14Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t)Pierre Letouzey
2017-06-14Remove support for Coq 8.2.Guillaume Melquiond
2017-06-12Remove more dead code (follow-up of previous commit).Théo Zimmermann
2017-06-09Fix Bug #5568, no dup notation warnings on repeated module importsPaul Steckler
2017-06-08Merge branch 'v8.6'Pierre-Marie Pédrot
2017-06-06Merge PR#662: Fixing bug #5233 and another bug with implicit arguments + a sh...Maxime Dénès
2017-06-06Merge PR#716: Don't double up on periods in anomaliesMaxime Dénès
2017-06-05Merge PR#590: A more explicit algebraic type for evars of kind MatchingVar + ...Maxime Dénès
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-06-01Merge PR#696: Trunk+cleanup constr of globalMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 17:20:41 +0000