aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/logic.mli
Commit message (Expand)AuthorAge
* [proof] Embed evar_map in RefinerError exception.Gravatar Emilio Jesus Gallego Arias2017-12-11
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* Merge PR #830: Moving assert (the "Cut" rule) to new proof engineGravatar Maxime Dénès2017-08-29
|\
* | Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
| * Exporting general-purpose functions on goal contexts from "logic.ml" to "tact...Gravatar Hugo Herbelin2017-06-25
|/
* Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
* Reductionops now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Termops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Moving "move" in the new proof engine.Gravatar Hugo Herbelin2016-09-24
* Adding a bit of documentation in the mli.Gravatar Pierre-Marie Pédrot2016-06-09
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
|/
* Update headers.Gravatar Maxime Dénès2015-01-12
* A version of convert_concl and convert_hyp in new proof engine.Gravatar Hugo Herbelin2014-10-09
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Algebraized "No such hypothesis" errorsGravatar Pierre-Marie Pédrot2014-01-06
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* Modulification of nameGravatar ppedrot2012-12-18
* Modulification of identifierGravatar ppedrot2012-12-14
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* Updating headers.Gravatar herbelin2012-08-08
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Raise informative errors instead of Failures or anomalies in case a metaGravatar msozeau2008-10-24
* Bugs, nettoyage, et améliorations diversesGravatar herbelin2008-04-13
* Correction du bug #1315:Gravatar notin2007-01-22
* Correction bug #842 (rename d'une hyp du contexte)Gravatar herbelin2006-03-01
* Correction erreur grossière de non restauration d'état en cas de retour exc...Gravatar herbelin2005-03-19
* restructuration des printers: proofs passe avant parsingGravatar barras2004-09-17
* deplacement de clenv vers pretypingGravatar barras2004-09-03
* premiere reorganisation de l\'unificationGravatar barras2004-09-03
* Nouvelle en-têteGravatar herbelin2004-07-16
* Légère amélioration des messages d'erreur des with-bindings et des RewriteGravatar herbelin2002-12-21
* Option pour rendre les vérifications du refiner optionnelleGravatar herbelin2002-12-09
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* Suppression des local_constraints, des ctxtty et du focus.Gravatar clrenard2001-11-06
* GROS COMMIT:Gravatar barras2001-11-05
* amelioration de la structure des universGravatar barras2001-03-28
* entetesGravatar filliatr2001-03-15
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* Ajout erreur DoesNotOccurInGravatar herbelin2000-12-06
* Abstraction de constrGravatar herbelin2000-09-14
* retablissement make doc et make minicoqGravatar filliatr2000-07-25
* Passage à des contextes de vars et de rels pouvant contenir des déclaration...Gravatar herbelin2000-07-24
* Effets de bords suite à la restructuration des inductives (cf Inductive)Gravatar herbelin2000-05-18