aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/logic.mli
Commit message (Expand)AuthorAge
* 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
* Ajout du langage de tactiquesGravatar delahaye2000-05-03
* rattrapage exceptions autres que UserErrorGravatar filliatr1999-12-14
* module PfeditGravatar filliatr1999-12-01
* - Typing -> Safe_typingGravatar filliatr1999-12-01
* modules Indrec, Tacentries, HiddentacGravatar filliatr1999-11-23
* module WcclausenvGravatar filliatr1999-11-22
* module Tactics (debut)Gravatar filliatr1999-11-22
* module Clenv (debut)Gravatar filliatr1999-10-20
* les variables existentielles contiennent maintenant un environnement (typeGravatar filliatr1999-10-19
* - déplacement (encore une fois !) des variables existentielles : elles sontGravatar filliatr1999-10-18
* module LogicGravatar filliatr1999-10-14
* module Proof_treesGravatar filliatr1999-10-14
* redeplacement des var. ex. dans kernel :-)Gravatar filliatr1999-10-13
* module Logic (ne compile pas encore)Gravatar filliatr1999-10-08