aboutsummaryrefslogtreecommitdiff
path: root/proofs/logic.ml
AgeCommit message (Expand)Author
2010-03-08Consider OccurCheck a catchable exception.msozeau
2010-01-04Errors issued by reduction tactics (e.g. pattern) were not caught by "try".herbelin
2009-10-25Add support for remaining side-conditions in "apply in as".herbelin
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-07-15- Fixing bug #2139 (kernel-based test of well-formation of eliminationherbelin
2009-06-06Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0herbelin
2009-05-23A try at using sort variables during unification. Instead of refreshingmsozeau
2009-02-19On remplace evar_map par evar_defs (seul evar_defs est désormais exporté aspiwack
2009-02-06pushed evar reduction in kernelbarras
2009-01-18Backporting from v8.2 to trunk:herbelin
2008-11-27fixing problem with CompCert: reordering resulting from tac change was not cl...barras
2008-11-26closed bug 1898: fold x in x; added a reordering primitive tacticbarras
2008-10-25Fix for bug #1981, correct the mismatch between the meta types used inmsozeau
2008-10-24Raise informative errors instead of Failures or anomalies in case a metamsozeau
2008-10-18Optimisation de clenv.ml pour que meta_instance ne soit pas appeléherbelin
2008-10-07fixing r11433 again:barras
2008-10-06bug #1951: polymorphic indtypes: universe subst was not performed in the type...barras
2008-09-09Correction bug assert (introduit dans la révision 11300) qui neherbelin
2008-09-07More debugging of [Equations], now able to discharge even the heavilymsozeau
2008-08-04Évolutions diverses et variées.herbelin
2008-06-27Changement de catch_error pour qu'il rattrape les erreurs d'arguments aspiwack
2008-04-30Réutilisation de l'infrastructure pour le polymorphisme d'univers desherbelin
2008-04-28Suite commit 10861herbelin
2008-04-28Petites corrections vis à vis des commits 10860, 10859, 10850herbelin
2008-04-13Bugs, nettoyage, et améliorations diversesherbelin
2008-04-04Mise en place d'une extension de apply pour que celui-ci sacheherbelin
2008-03-10Une passe sur l'unification des evars (suite aux commits 10124, 10125, 10145)herbelin
2007-12-07Util.option_compare devient Option.Misc.Compare et change un peu de type aspiwack
2007-12-06Plus de combinateurs sont passés de Util à Option. Le module Options aspiwack
2007-09-06Uniformisation politique de nommage evd/isevars (evd si evar_defs,herbelin
2007-05-29Correction d'un bug dans l'affichage du message d'erreur real_cleanherbelin
2007-04-28Correction bug #1519herbelin
2007-03-15Suppression argument pattern_source du case_info (code jamais utilisé)herbelin
2007-01-31Correction d'un bug dans check_and_clear_in_constr + simplification denotin
2007-01-30Nouvelle implantation de clear_hypsnotin
2007-01-22Correction du bug #1315:notin
2006-10-30Débranchement du polymorphisme de sorte sur les définitions dans Typeherbelin
2006-10-29Compatibilité du polymorphisme de constantes avec les sections.herbelin
2006-10-28Extension du polymorphisme de sorte au cas des définitions dans Type.herbelin
2006-10-03Changement de comportement du [rewrite ... in H]: Coq échoue si Hnotin
2006-09-20Declarative Proof Language: main commitcorbinea
2006-05-28- Indtypes: en attente opinion CoRN, les occurrences de Type non explicitesherbelin
2006-04-11patch pour contourner l'échec de type_of_applied_inductive sur un inductif a...herbelin
2006-03-29Inductifs avec polymorphisme de sorte (version initiale)herbelin
2006-03-24Patch envoy\'e par Benjamin Gregoire, permettant de corrigerletouzey
2006-03-01Correction bug #842 (rename d'une hyp du contexte)herbelin
2005-12-17Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...herbelin
2005-12-02Changement des named_contextgregoire
2005-10-27catchable_exception laisse passer les InductiveErrorwerner
2005-07-13Correction double bug #986: Fold ne préserve pas nécessairement le typage e...herbelin