aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/logic.ml
Commit message (Expand)AuthorAge
...
* Fixing #2968. This is quite brittle though, because we are messingGravatar ppedrot2013-04-16
* Allow catching of WrongAbstractionType, fixing a regression from 8.4Gravatar msozeau2013-04-05
* Restrict (try...with...) to avoid catching critical exn (part 12)Gravatar letouzey2013-03-13
* Removing Exc_located and using the new exception enrichementGravatar ppedrot2013-02-18
* Added propagation of evars unification failure reasons for betterGravatar herbelin2013-02-17
* Revised the Ltac trace mechanism so that trace breaking due toGravatar herbelin2013-02-17
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
* Modulification of nameGravatar ppedrot2012-12-18
* Modulification of identifierGravatar ppedrot2012-12-14
* Renamed Option.Misc.compare to the more uniform Option.equal.Gravatar ppedrot2012-12-13
* Monomorphization (proof)Gravatar ppedrot2012-11-25
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* As r15801: putting everything from Util.array_* to CArray.*.Gravatar ppedrot2012-09-14
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* The new ocaml compiler (4.00) has a lot of very cool warnings,Gravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* Glob_term now mli-only, operations now in Glob_opsGravatar letouzey2012-05-29
* Tacexpr as a mli-only, the few functions there are now in TacopsGravatar letouzey2012-05-29
* Noise for nothingGravatar pboutill2012-03-02
* Fixes bug #2654 (tactic instantiate failing to update existential variables).Gravatar aspiwack2012-01-06
* Granted legitimate wish #2607 (not exposing crude fixpoint body ofGravatar herbelin2011-12-18
* Propagated information from the reduction tactics to the kernel soGravatar herbelin2011-08-10
* Extraction: forbid Prop-polymorphism of inductives when extracting to OcamlGravatar letouzey2011-07-04
* Catch AbstractionOverMeta as a unification failure in precatchable_exception.Gravatar msozeau2011-06-07
* Reverted commit r13893 about propagation of more informativeGravatar herbelin2011-03-07
* Added propagation of evars unification failure reasons for betterGravatar herbelin2011-03-07
* Attempt to preserve casts during a refine, especially VMcastGravatar letouzey2010-12-10
* Delayed the evar normalization in error messages to the last minuteGravatar herbelin2010-11-07
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Applied Pierre Letouzey's patch restoring Convert_concl VM casts in new proofGravatar herbelin2010-07-21
* Automatic introduction of names given before ":" in Lemma's andGravatar herbelin2010-06-09
* Add (almost) compatibility with camlp4, without breaking support for camlp5Gravatar letouzey2010-05-19
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
* Consider OccurCheck a catchable exception.Gravatar msozeau2010-03-08
* Errors issued by reduction tactics (e.g. pattern) were not caught by "try".Gravatar herbelin2010-01-04
* Add support for remaining side-conditions in "apply in as".Gravatar herbelin2009-10-25
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* - Fixing bug #2139 (kernel-based test of well-formation of eliminationGravatar herbelin2009-07-15
* Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0Gravatar herbelin2009-06-06
* A try at using sort variables during unification. Instead of refreshingGravatar msozeau2009-05-23
* On remplace evar_map par evar_defs (seul evar_defs est désormais exporté Gravatar aspiwack2009-02-19
* pushed evar reduction in kernelGravatar barras2009-02-06
* Backporting from v8.2 to trunk:Gravatar herbelin2009-01-18
* fixing problem with CompCert: reordering resulting from tac change was not cl...Gravatar barras2008-11-27
* closed bug 1898: fold x in x; added a reordering primitive tacticGravatar barras2008-11-26