aboutsummaryrefslogtreecommitdiff
path: root/proofs/logic.ml
AgeCommit message (Expand)Author
2020-07-01UIP in SPropGaëtan Gilbert
2020-06-24Remove the catchable-exception related functions.Pierre-Marie Pédrot
2020-05-12Write the outermost part of the legacy refiner directly in the monad.Pierre-Marie Pédrot
2020-05-12Clean up the legacy refiner implementation.Pierre-Marie Pédrot
2020-05-12Remove legacy Refiner error constructors.Pierre-Marie Pédrot
2020-05-12Wrap the legacy refiner type into the Logic API.Pierre-Marie Pédrot
2020-05-12Do not use Unsafe.to_constr for old refiner conclusion.Pierre-Marie Pédrot
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-02-06unsafe_type_of -> type_of in Logic.check_typabilityGaëtan Gilbert
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-10Fast-path for reordering of a single closed variable.Pierre-Marie Pédrot
2019-05-10Split the hypothesis conversion check in a conversion + ordering check.Pierre-Marie Pédrot
2019-05-10Logic.convert_hyp now takes an environment as an argument.Pierre-Marie Pédrot
2019-05-10Cleanup of Logic.convert_hyp.Pierre-Marie Pédrot
2019-04-05[api] [proofs] Remove dependency of proofs on interp.Emilio Jesus Gallego Arias
2018-12-12Merge PR #8965: Add `String Notation` vernacular like `Numeral Notation`Hugo Herbelin
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-11-28Factor out common code in numeral/string notationsJason Gross
2018-11-21[legacy proof engine] Remove some cruft.Emilio Jesus Gallego Arias
2018-11-19[proof] Provide better control of "open proofs" exceptions.Emilio Jesus Gallego Arias
2018-10-31Renaming is_template_polymorphic -> is_template_polymorphic_ind.Hugo Herbelin
2018-10-30Avoid passing dummy env to error printerMaxime Dénès
2018-10-26Cleanup evar_extra: remove evar_info's store and add maps to evar_mapMatthieu Sozeau
2018-10-14Passing env functionally in move_hyp and insert_decl_in_named_context.Hugo Herbelin
2018-09-19Fix Numeral Notations (2/4 - exceptions, usr_err)Jason Gross
2018-06-12[api] Misctypes removal: several moves:Emilio Jesus Gallego Arias
2018-06-04Stronger invariants in unification signature.Pierre-Marie Pédrot
2018-05-23Collecting Array.smart_* functions into a module Array.Smart.Hugo Herbelin
2018-03-29Preparing old-style refine from logic.ml to deal with "Cases" proofHugo Herbelin
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-02Reductionops.nf_* now take an environment.Gaëtan Gilbert
2017-12-11[proof] Embed evar_map in RefinerError exception.Emilio Jesus Gallego Arias
2017-11-22[api] Deprecate Term destructors, move to ConstrEmilio Jesus Gallego Arias
2017-11-13[api] Another large deprecation, `Nameops`Emilio Jesus Gallego Arias
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-08-29Merge PR #830: Moving assert (the "Cut" rule) to new proof engineMaxime Dénès
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-25Moving "assert" (internally "Cut") to the new proof engine.Hugo Herbelin
2017-06-25Exporting general-purpose functions on goal contexts from "logic.ml" to "tact...Hugo Herbelin
2017-06-13Improving documentation of tactic "move" (report #4561).Hugo Herbelin
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-05-27[cleanup] Unify all calls to the error function.Emilio Jesus Gallego Arias
2017-05-03Merge PR#411: Mention template polymorphism in the documentation.Maxime Dénès
2017-04-27Remove some unused values and typesGaetan Gilbert
2017-04-11Update various comments to use "template polymorphism"Gaetan Gilbert
2017-04-01Using delayed universe instances in EConstr.Pierre-Marie Pédrot
2017-03-29Fix call to broken unsafe_type_of in apply tactic.Maxime Dénès
2017-02-14Definining EConstr-based contexts.Pierre-Marie Pédrot
2017-02-14Removing various compatibility layers of tactics.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:33:45 +0000