aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-06-20Fix bug #4825: [clear] should not dependency-check hypotheses that come above...Pierre-Marie Pédrot
2016-06-20Prevent a useless evar normalization in Clenvtac.unify.Pierre-Marie Pédrot
2016-06-20Do not evar-normalize goals when interpreting some hardwired genargs.Pierre-Marie Pédrot
2016-06-19Merge 'pr/215' into trunkEnrico Tassi
2016-06-19Fix bug #4836: Anomaly: Uncaught exception Invalid_argument.Pierre-Marie Pédrot
2016-06-18Fix path separator on windowsJason Gross
2016-06-18Fix the build on WindowsJason Gross
2016-06-18Merge PR# 169: Local type-in-type flag.Pierre-Marie Pédrot
2016-06-18Fixing the checker.Pierre-Marie Pédrot
2016-06-18Reuse the typing_flags datatype for inductives.Pierre-Marie Pédrot
2016-06-18Moving the typing_flags to the environment.Pierre-Marie Pédrot
2016-06-18Print the type-in-type flag in various user-facing functions.Pierre-Marie Pédrot
2016-06-18Adding a local type-in-type flag in kernel declarations.Pierre-Marie Pédrot
2016-06-18Test-suite fix to 1744e37 (injection in context).Hugo Herbelin
2016-06-18Backporting c064fb933 from 8.5 (another regression with Ltac trace report).Hugo Herbelin
2016-06-18Adding an "as" clause to specialize.Hugo Herbelin
2016-06-18Giving a more natural semantics to injection by default.Hugo Herbelin
2016-06-18Exporting a generic argument induction_arg. As a consequence,Hugo Herbelin
2016-06-18A cleaning phase around delayed induction arg + exporting force_induction_arg.Hugo Herbelin
2016-06-18Adding eintros to respect the e- prefix policy.Hugo Herbelin
2016-06-17par: like all: but in parallelEnrico Tassi
2016-06-17remote counter: avoid thread race on sockets (fix #4823)Enrico Tassi
2016-06-17Mentioning goal selectors in CHANGESEnrico Tassi
2016-06-16Merge branch 'nzgcd' into trunkMatthieu Sozeau
2016-06-16Remove unneded hints in NZGcdMatthieu Sozeau
2016-06-16proof mode: print unification constraintsMatthieu Sozeau
2016-06-16Tentative fix of test-suite file to avoid loopMatthieu Sozeau
2016-06-16Typeclasses:rename solve_instantiation* & use HookMatthieu Sozeau
2016-06-16Fix resolve_one_typeclass to use the new engineMatthieu Sozeau
2016-06-16Bind resolve_one_typeclass to 8.5 or 8.6 resolutionMatthieu Sozeau
2016-06-16Fix wrong tabulation in CHANGESMatthieu Sozeau
2016-06-16Put autoapply back, lost during rebaseMatthieu Sozeau
2016-06-16Cleanup and refactoringMatthieu Sozeau
2016-06-16Document new Hint Mode option.Matthieu Sozeau
2016-06-16Extend Hint Mode to handle the no-head-evar caseMatthieu Sozeau
2016-06-16Revise syntax of Hint CutMatthieu Sozeau
2016-06-16Example given at DeepSpec workshopMatthieu Sozeau
2016-06-16Purely refactoring and code/API cleanup.Matthieu Sozeau
2016-06-16eauto: fix test-suite fileMatthieu Sozeau
2016-06-16bteauto: a Proofview.tactic for multiple goalsMatthieu Sozeau
2016-06-16Typeclasses: allow shelved subgoalsMatthieu Sozeau
2016-06-16Minor cleanupMatthieu Sozeau
2016-06-16Typeclasses: refine the eauto tacticMatthieu Sozeau
2016-06-16Typeclasses: verbosity and Limit Intros optionsMatthieu Sozeau
2016-06-16Proofview: extensions for backtracking eautoMatthieu Sozeau
2016-06-16typeclass resolution: add two compatibility optionsMatthieu Sozeau
2016-06-16setoid_rewrite: fix the Params resolution tacticMatthieu Sozeau
2016-06-16Fix incorrect caching of local hints w.r.t sectionsMatthieu Sozeau
2016-06-16Compat with ocaml 4.01Matthieu Sozeau
2016-06-16Fix iterative deepening strategy failing too earlyMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 11:28:53 +0000