aboutsummaryrefslogtreecommitdiff
path: root/engine
AgeCommit message (Expand)Author
2017-01-23Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-12-02Document changesMatthieu Sozeau
2016-11-30Fix UGraph.check_eq!Matthieu Sozeau
2016-11-07Merge remote-tracking branch 'github/pr/339' into v8.6Maxime Dénès
2016-11-07Fixes to compile with ocaml 4.01Matthieu Sozeau
2016-11-07Merge commit 'e6edb33' into v8.6Maxime Dénès
2016-10-28Merge remote-tracking branch 'github/pr/321' into v8.6Maxime Dénès
2016-10-26Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-10-22Unification constraint handling (#4763, #5149)Matthieu Sozeau
2016-10-21Oops, my bad, didn't expect a merge issue!Matthieu Sozeau
2016-10-21Merge remote-tracking branch 'gforge/v8.5' into v8.6Matthieu Sozeau
2016-10-21sections/hints: prevent Not_found in get_type_ofMatthieu Sozeau
2016-10-15Fix bug #5145: Anomaly: index to an anonymous variable.Pierre-Marie Pédrot
2016-10-12Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-10-12Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-10-03Merge remote-tracking branch 'github/pr/263' into v8.6Maxime Dénès
2016-09-16Adding variants enter_one and refine_one which assume that exactly oneHugo Herbelin
2016-09-09Tracking careless uses of slow name lookup.Pierre-Marie Pédrot
2016-09-05Fast path in push_rel_context_to_named_context.Pierre-Marie Pédrot
2016-09-02Fast path in whd_evar.Pierre-Marie Pédrot
2016-09-01Short documentation, filling TODO's in evd.mli.Hugo Herbelin
2016-08-25Do not export an internal function in Namegen.Pierre-Marie Pédrot
2016-08-17Two protections against failures when printing evar_map.Hugo Herbelin
2016-08-17Fixing printing in debugger (no global env in debugger).Hugo Herbelin
2016-08-16Efficiently generate the pretyping contexts.Pierre-Marie Pédrot
2016-08-10Remove unused optional "predicative" argument.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-04Use sets instead of lists for names to avoid in evar generation.Pierre-Marie Pédrot
2016-08-04Simplifying code in evar generation.Pierre-Marie Pédrot
2016-08-04Exporting the renaming API for evar declaration.Pierre-Marie Pédrot
2016-07-08Fixing #4906 (regression in printing an error message).Hugo Herbelin
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-29Univ: Use loc even if there are more unbound levelsMatthieu Sozeau
2016-06-29Univs: add source locations of levelsMatthieu Sozeau
2016-06-24Optmimize the subst tactic.Pierre-Marie Pédrot
2016-06-24Optimize the clear tactic.Pierre-Marie Pédrot
2016-06-24Optimize the clear tactic.Pierre-Marie Pédrot
2016-06-23Better algorithm for variable deambiguation in term printing.Pierre-Marie Pédrot
2016-06-16Document new Hint Mode option.Matthieu Sozeau
2016-06-16Proofview: extensions for backtracking eautoMatthieu Sozeau
2016-06-16Implement limited proof search and iterative deepening.Matthieu Sozeau
2016-06-16Merge 'pr/191' into trunkEnrico Tassi
2016-06-14Merge remote-tracking branch 'origin/pr/173' into trunkEnrico Tassi
2016-06-14Fix a typo in proofs/proofview.mli.Cyprien Mangin
2016-06-14Fix usage of Pervasives in goal selectors.Cyprien Mangin
2016-06-14Add a comment about the use of a zipper, for clarity.Cyprien Mangin
2016-06-14Add a [CList.partitioni] function.Cyprien Mangin
2016-06-14Add goal range selectors.Cyprien Mangin
2016-06-09Adding a bit of documentation in the mli.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:44:39 +0000