aboutsummaryrefslogtreecommitdiff
path: root/engine
AgeCommit message (Expand)Author
2018-03-08Merge PR #6893: Cleanup UState API usageMaxime Dénès
2018-03-08Merge PR #6899: [compat] Remove "Standard Proposition Elimination"Maxime Dénès
2018-03-08Merge PR #6582: Mangle auto-generated namesMaxime Dénès
2018-03-06Rename some universe minimizing "normalize" functions to "minimize"Gaëtan Gilbert
2018-03-06Deprecate UState aliases in Evd.Gaëtan Gilbert
2018-03-05Add empty description for @raise statements to satisfy ocamldocmrmr1993
2018-03-05Replace invalid tag @raises in ocamldoc comments with @raisemrmr1993
2018-03-05Tweak comments to fix ocamldoc errorsmrmr1993
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-04Proofview: V82.tactic option to not normalize evarsEnrico Tassi
2018-03-04proofview: debug API to print a goalEnrico Tassi
2018-03-04Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.Maxime Dénès
2018-03-04Merge PR #6676: [proofview] goals come with a stateMaxime Dénès
2018-03-03[compat] Remove "Standard Proposition Elimination"Emilio Jesus Gallego Arias
2018-02-28[econstr] Continue consolidation of EConstr API under `interp`.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-27Add a comment on EConstr.to_constr regarding evar-freeness.Pierre-Marie Pédrot
2018-02-22[ast] Improve precision of Ast location recognition in serialization.Emilio Jesus Gallego Arias
2018-02-20proofview: goals come with a stateEnrico Tassi
2018-02-17Implement name mangling optionJasper Hugunin
2018-02-12[engine] Remove ghost parameter from `Proofview.Goal.t`Emilio Jesus Gallego Arias
2018-02-12Merge PR #6262: [error] Replace msg_error by a proper exception.Maxime Dénès
2018-02-10Simplification: cumulativity information is variance information.Gaëtan Gilbert
2018-02-09[error] Replace msg_error by a proper exception.Emilio Jesus Gallego Arias
2018-02-01Merge PR #6675: [proofview] enter_one: add __LOC__ argument to get relevant e...Maxime Dénès
2018-01-31Proofview: enter_one: add __LOC__ argument to get relevant error msgEnrico Tassi
2018-01-31Merge PR #6535: Cleanup name-binding structure for fresh evar name generation.Maxime Dénès
2018-01-22Merge PR #6618: Fix Ltac subterm matching in (co-)fixpoints.Maxime Dénès
2018-01-19Define EConstr version of [push_rec_types].Cyprien Mangin
2018-01-18Merge PR #6555: Use let-in aware prod_applist_assum in dtauto and firstorder.Maxime Dénès
2018-01-17Merge PR #6298: Fix #6297: handle constraints like (u+1 <= Set/Prop)Maxime Dénès
2018-01-17Add a test that `prod_applist_assum` reduces the right number of let-insJasper Hugunin
2018-01-17Use let-in aware prod_applist_assum in dtauto and firstorder.Jasper Hugunin
2018-01-04Use a more efficient substitution composition in evar hypothesis naming.Pierre-Marie Pédrot
2018-01-02Cleanup name-binding structure for fresh evar name generation.Pierre-Marie Pédrot
2017-12-30Moving some universe substitution code out of the kernel.Pierre-Marie Pédrot
2017-12-22Merge PR #6222: Share computation of unifiable evarsMaxime Dénès
2017-12-18Merge PR #6413: [econstr] Switch constrintern API to non-imperative style.Maxime Dénès
2017-12-15Merge PR #6392: [econstr] Cleanup in `vernac/classes.ml`Maxime Dénès
2017-12-14Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.Maxime Dénès
2017-12-13[econstr] Add a couple of new API functions.Emilio Jesus Gallego Arias
2017-12-13[econstr] Cleanup in `vernac/classes.ml`.Emilio Jesus Gallego Arias
2017-12-12Merge PR #6275: [summary] Allow typed projections from global state.Maxime Dénès
2017-12-11Merge PR #6368: [api] Remove yet another type alias.Maxime Dénès
2017-12-11Merge PR #6324: Fix #6323: stronger restrict universe context vs abstract.Maxime Dénès
2017-12-09[api] Remove yet another type alias.Emilio Jesus Gallego Arias
2017-12-09[lib] Rename Profile to CProfileEmilio Jesus Gallego Arias
2017-12-09[summary] Adapt STM to the new Summary API.Emilio Jesus Gallego Arias
2017-12-07Merge PR #6290: Rename update to set, Fixes #6196Maxime Dénès
2017-12-06Fix #6323: stronger restrict universe context vs abstract.Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 13:17:33 +0000