aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-01-11COMMENTS: of "Constr.case_info" type were updated.Matej Kosik
2016-01-11COMMENTS: added to the "Names.inductive" and "Names.constructor" types.Matej Kosik
2016-01-09Fix bug 4479: "Error: Rewriting base foo does not exist." should be catchable.Pierre-Marie Pédrot
2016-01-08Monotonizing Ftactic.Pierre-Marie Pédrot
2016-01-08Be more verbose about failure to compile libraries to native code.Guillaume Melquiond
2016-01-07Fix a misleading comment for substn_varsMatthieu Sozeau
2016-01-07Fix bug #4480: progress was not checked for setoid_rewrite.Matthieu Sozeau
2016-01-06Fix description of command-line options in the manual.Guillaume Melquiond
2016-01-06Remove deprecated command-line options such as "-as".Guillaume Melquiond
2016-01-06Make code more readable by not mixing list traversal and option processing.Guillaume Melquiond
2016-01-06Merge remote-tracking branch 'origin/v8.5' into trunkGuillaume Melquiond
2016-01-06Prevent coq_makefile from parsing project files in the reverse order. (Fix bu...Guillaume Melquiond
2016-01-06Protect code against changes in Map interface.Maxime Dénès
2016-01-05Disable warning 31 when generating coqtop from coqmktop.Maxime Dénès
2016-01-05Merge remote-tracking branch 'origin/v8.5' into trunkGuillaume Melquiond
2016-01-05Avoid warning 31: test printer was linked twice with Dynlink and Str.Maxime Dénès
2016-01-05Fix order of files in mllib.Maxime Dénès
2016-01-05COMMENTS: PredicateMatej Kosik
2016-01-04fixup d2b468a, evar normalization is neededEnrico Tassi
2016-01-04Extraction: msg_notice instead of msg_info.Pierre Courtieu
2016-01-04Fix handling of side-effects in case of `Opaque side-effects as well.Matthieu Sozeau
2016-01-04par: check if the goal is not ground and fail (fix #4465)Enrico Tassi
2016-01-04workers: purge short version of -load-vernac too (fix #4458)Enrico Tassi
2016-01-02Use streams rather than strings to handle bullet suggestions.Guillaume Melquiond
2016-01-02Remove some unused functions.Guillaume Melquiond
2016-01-02Remove keys for evar and meta, since they cannot occur.Guillaume Melquiond
2016-01-02Remove some useless type declarations.Guillaume Melquiond
2016-01-02Remove some useless module opening.Guillaume Melquiond
2016-01-02Remove duplicate definition.Guillaume Melquiond
2016-01-02Remove duplicate declarations.Guillaume Melquiond
2016-01-02Reduce dependencies of interface files.Guillaume Melquiond
2016-01-02Avoid warnings about loop indices.Guillaume Melquiond
2016-01-02Remove useless rec flags.Guillaume Melquiond
2016-01-02Simplification of grammar_prod_item type.Pierre-Marie Pédrot
2016-01-02Proper datatype for EXTEND syntax tokens.Pierre-Marie Pédrot
2016-01-02Separation of concern in TacAlias API.Pierre-Marie Pédrot
2016-01-01Fix typos.Guillaume Melquiond
2016-01-01Remove unused hashconsing code.Guillaume Melquiond
2016-01-01Do not make it harder on the compiler optimizer by packing arguments.Guillaume Melquiond
2016-01-01Remove unused functions.Guillaume Melquiond
2016-01-01Remove unplugged button from the interface.Guillaume Melquiond
2016-01-01Remove useless recursive flags.Guillaume Melquiond
2016-01-01Remove unused open.Guillaume Melquiond
2016-01-01Remove duplicate declarations.Guillaume Melquiond
2015-12-31Put implicits back as in 8.4.Matthieu Sozeau
2015-12-31Fix bug #4456, anomaly in handle-side effectsMatthieu Sozeau
2015-12-31Remove unused function Checker.print_loc.Guillaume Melquiond
2015-12-31Merge branch 'v8.5' into trunkGuillaume Melquiond
2015-12-31Do not compose List.length with List.filter.Guillaume Melquiond
2015-12-31Remove Library.mem, which is pointless since 8.5.Guillaume Melquiond
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-16 08:06:18 +0000