aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2016-10-07Fix bug #4464: "Anomaly: variable H' unbound. Please report.".Pierre-Marie Pédrot
2016-10-04Quick fix to #4595 (making notations containing "ltac:" unused for printing).Hugo Herbelin
2016-10-03Merge remote-tracking branch 'github/pr/263' into v8.6Maxime Dénès
2016-09-28Fix bug #4723 and FIXME in API for solve_by_tacMatthieu Sozeau
2016-09-28Remove incorrect assertion in cbn (bug #4822).Guillaume Melquiond
2016-09-26Posssible abstractions over goal variables when inferring match return clause.Hugo Herbelin
2016-09-26Trying an abstracting dependencies heuristic for the match return clause even...Hugo Herbelin
2016-09-26Trying a no-inversion no-dependency heuristic for match return clause.Hugo Herbelin
2016-09-26Inference of return clause: giving uniformly priority to "small inversion".Hugo Herbelin
2016-09-23Fix bug #5096: [vm_compute] is exponentially slower than [native_compute].Pierre-Marie Pédrot
2016-09-23Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-09-22Fixing #5095 (non relevant too strict test in let-in abstraction).Hugo Herbelin
2016-09-14Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-09-12Merge remote-tracking branch 'github-coq/pr/249' into v8.6Matthieu Sozeau
2016-09-10Fixing #5077 (failure on typing a fixpoint with evars in its type).Hugo Herbelin
2016-09-09no-refold patchPaul Steckler
2016-09-09Fast path in Clenvtac.clenv_refine typeclass resolution.Pierre-Marie Pédrot
2016-09-09Monomorphize a costly boolean equality operation.Pierre-Marie Pédrot
2016-09-09Tracking careless uses of slow name lookup.Pierre-Marie Pédrot
2016-08-24Merge PR #258: "Fix newline issues" into v8.6Pierre-Marie Pédrot
2016-08-22Pushing error backtrace in unification reraise.Pierre-Marie Pédrot
2016-08-21Do not recompute the whole evar naming environment in GProd intepretation.Pierre-Marie Pédrot
2016-08-21Short path for Pretyping.ltac_interp_name_env.Pierre-Marie Pédrot
2016-08-20Fixing a bug in the presence of let-in while inferring the return clause.Hugo Herbelin
2016-08-19[pp] Fix newline issues.Emilio Jesus Gallego Arias
2016-08-17Two protections against failures when printing evar_map.Hugo Herbelin
2016-08-16Efficiently generate the pretyping contexts.Pierre-Marie Pédrot
2016-08-10Make it a bit more obvious when variables are of type unit.Guillaume Melquiond
2016-08-06Using a dedicated kind of substitutions in evar name generation.Pierre-Marie Pédrot
2016-08-05Using the extended contexts in pretyping.Pierre-Marie Pédrot
2016-08-04Embedding the pretyping environment in a dummy record.Pierre-Marie Pédrot
2016-07-18A new step on using alpha-conversion in printing notations.Hugo Herbelin
2016-07-17Partial fix to #4592 (notation requiring alpha-conversion for printing).Hugo Herbelin
2016-07-08Remove spurious warnings about projections when requiring modules.Pierre-Marie Pédrot
2016-07-07Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-07-07Merge remote-tracking branch 'github/bug4653' into v8.6Matthieu Sozeau
2016-07-06Fix reopened bug #3317.Matthieu Sozeau
2016-07-06Disallow dependent case on prim records w/o etaMatthieu Sozeau
2016-07-06Renaming to more generic has_dependent_elim testMatthieu Sozeau
2016-07-06Move is_prim... to Inductiveops and correct SchemeMatthieu Sozeau
2016-07-06Univs: fix internalization of (x := T) and castsMatthieu Sozeau
2016-07-04Merge branch 'v8.5' into trunkMaxime Dénès
2016-07-04congruence: Restrict refreshing to SetMatthieu Sozeau
2016-07-04congruence/univs: properly refresh (fix #4609)Matthieu Sozeau
2016-07-03closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)Pierre Letouzey
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-07-01Add and document match, fix and cofix reduction flags.Maxime Dénès
2016-07-01Make semantics of whd_zeta consistent with other whd_* functions.Maxime Dénès
2016-07-01Separate flags for fix/cofix/match reduction and clean reduction function names.Maxime Dénès
2016-06-29Program: cleanup in cases, add optionsMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 18:06:21 +0000