aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-01-12Fix essential bug in new Keyed Unification mode reported by R. Krebbers.Matthieu Sozeau
2016-01-12Referring to coq.inria.fr/stdlib for more on libraries and ltac-level tactics.Hugo Herbelin
2016-01-12Documenting dtauto and dintuition.Hugo Herbelin
2016-01-12Documenting options "Intuition Negation Unfolding", "Intuition Iff Unfolding".Hugo Herbelin
2016-01-12Documenting option 'Set Bracketing Last Introduction Pattern'.Hugo Herbelin
2016-01-12restore documentation of admitEnrico Tassi
2016-01-11CLEANUP: removing unnecessary wrapperMatej Kosik
2016-01-11COMMENTS: added to the "Constrexpr.CCases" variant.Matej Kosik
2016-01-11CLEANUP: removing unused fieldMatej Kosik
2016-01-11mergeMatej Kosik
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2016-01-11Fix bug #3338 again, no progress is necessary for the success of rewrite_strat.Matthieu Sozeau
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-08 07:52:13 +0000