aboutsummaryrefslogtreecommitdiff
path: root/tactics/decl_interp.ml
AgeCommit message (Expand)Author
2009-11-09A bit of cleaning around name generation + creation of dedicated file namegen.mlherbelin
2009-10-27fixed czar bug with parametric inductivescorbinea
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-04-08Some dead code removal + cleanupsletouzey
2008-10-22Affichage des notations récursives:herbelin
2008-09-07Better handling of the opacity of proof obligations, add the possibility ofmsozeau
2008-07-17Uniformisation du format des messages d'erreur (commencent par uneherbelin
2008-04-01Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientherbelin
2007-12-31Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...msozeau
2007-12-05Factorisation des opérations sur le type option de Util dans un module aspiwack
2007-11-08Prise en compte des notations "alias" dans la globalisation des coercions.herbelin
2007-04-26fin des conclusions multiplescorbinea
2007-03-19Add a parameter to QuestionMark evar kind to say it can be turned into an obl...msozeau
2007-01-29bugfix for suffices (support for open head)corbinea
2007-01-29finalized sufficescorbinea
2007-01-28"suffices" implemented + syntax cleanupcorbinea
2007-01-25decl mode: anonymous factscorbinea
2007-01-22changes in declarative language : by term using tacticcorbinea
2006-09-20Declarative Proof Language: main commitcorbinea
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 15:03:12 +0000