aboutsummaryrefslogtreecommitdiff
path: root/engine
AgeCommit message (Expand)Author
2016-09-16Adding variants enter_one and refine_one which assume that exactly oneHugo Herbelin
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
2016-06-06STM: proof block detection for bullets and { block }Enrico Tassi
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-05-20Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-05-04Normalizing the names of dynamic types to follow a typ_* scheme.Pierre-Marie Pédrot
2016-05-04Interpretation function can return any untyped value.Pierre-Marie Pédrot
2016-05-04Removing external uses of Val.inject and making Geninterp.interp return Val.tPierre-Marie Pédrot
2016-05-04Moving the Val module to Geninterp.Pierre-Marie Pédrot
2016-05-04Getting rid of the Geninterp.generic_interp function.Pierre-Marie Pédrot
2016-05-04Switching to an untyped toplevel representation for Ltac values.Pierre-Marie Pédrot
2016-05-04Moving Ftactic and Geninterp to the engine folder.Pierre-Marie Pédrot
2016-03-20Moving Evarutil and Proofview to engine/Pierre-Marie Pédrot
2016-03-20Making Proofview independent of Logic.Pierre-Marie Pédrot
2016-02-19Allowing to attach location to universes in UState.Pierre-Marie Pédrot
2016-02-15merging conflicts with the original "trunk__CLEANUP__Context__2" branchMatej Kosik
2016-02-15Monotonizing the Evarutil module.Pierre-Marie Pédrot
2016-02-13Merge branch 'v8.5'Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:07:17 +0000