aboutsummaryrefslogtreecommitdiff
path: root/proofs/logic.mli
AgeCommit message (Expand)Author
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
2004-07-16Nouvelle en-têteherbelin
2002-12-21Légère amélioration des messages d'erreur des with-bindings et des Rewriteherbelin
2002-12-09Option pour rendre les vérifications du refiner optionnelleherbelin
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2001-11-06Suppression des local_constraints, des ctxtty et du focus.clrenard
2001-11-05GROS COMMIT:barras
2001-03-28amelioration de la structure des universbarras
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:22:34 +0000