aboutsummaryrefslogtreecommitdiff
path: root/proofs/logic.mli
AgeCommit message (Expand)Author
2020-06-24Remove the catchable-exception related functions.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-19Merge PR #11735: Deprecating catchable_exceptionPierre-Marie Pédrot
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-13Deprecation of catchable_exception, to be replaced by noncritical in try-with.Hugo Herbelin
2019-06-17Update ml-style headers to new year.Théo Zimmermann
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
2018-11-21[legacy proof engine] Remove some cruft.Emilio Jesus Gallego Arias
2018-10-14Passing env functionally in move_hyp and insert_decl_in_named_context.Hugo Herbelin
2018-06-12[api] Misctypes removal: several moves:Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2017-12-11[proof] Embed evar_map in RefinerError exception.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-25Exporting general-purpose functions on goal contexts from "logic.ml" to "tact...Hugo Herbelin
2017-02-14Definining EConstr-based contexts.Pierre-Marie Pédrot
2017-02-14Reductionops now return EConstrs.Pierre-Marie Pédrot
2017-02-14Termops API using EConstr.Pierre-Marie Pédrot
2016-09-24Moving "move" in the new proof engine.Hugo Herbelin
2016-06-09Adding a bit of documentation in the mli.Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2015-01-12Update headers.Maxime Dénès
2014-10-09A version of convert_concl and convert_hyp in new proof engine.Hugo Herbelin
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-01-06Algebraized "No such hypothesis" errorsPierre-Marie Pédrot
2013-04-29Merging Context and Sign.ppedrot
2012-12-18Modulification of nameppedrot
2012-12-14Modulification of identifierppedrot
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-08-08Updating headers.herbelin
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2010-04-22Here comes the commit, announced long ago, of the new tactic engine.aspiwack
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2008-10-24Raise informative errors instead of Failures or anomalies in case a metamsozeau
2008-04-13Bugs, nettoyage, et améliorations diversesherbelin
2007-01-22Correction du bug #1315:notin
2006-03-01Correction bug #842 (rename d'une hyp du contexte)herbelin
2005-03-19Correction erreur grossière de non restauration d'état en cas de retour exc...herbelin
2004-09-17restructuration des printers: proofs passe avant parsingbarras
2004-09-03deplacement de clenv vers pretypingbarras
2004-09-03premiere reorganisation de l\'unificationbarras
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:02:32 +0000