aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/logic.mli
Commit message (Expand)AuthorAge
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 02:37:20 +0000