aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Expand)AuthorAge
* Added a command "Unfocused" which returns an error when the proof isGravatar aspiwack2012-03-30
* info_trivial, info_auto, info_eauto, and debug (trivial|auto)Gravatar letouzey2012-03-30
* Remove code of obsolete tactics : superauto, autotdb, cdhyp, dhyp, dconclGravatar letouzey2012-03-30
* A unified backtrack mechanism, with a basic "Show Script" as side-effectGravatar letouzey2012-03-23
* Remove old proof-managment commands Suspend/ResumeGravatar letouzey2012-03-23
* Pfedit: avoid Undoing too muchGravatar letouzey2012-03-21
* Fix interface of resolve_typeclasses: onlyargs -> with_goals:Gravatar msozeau2012-03-20
* Arranged for the desirable behaviour that bullets do not see beyond braces.Gravatar aspiwack2012-03-20
* Fixing alpha-conversion bug #2723 introduced in r12485-12486.Gravatar herbelin2012-03-20
* Revise API of understand_ltac to be parameterized by a flag for resolution of...Gravatar msozeau2012-03-14
* Integrated obligations/eterm and program well-founded fixpoint building to to...Gravatar msozeau2012-03-14
* Second step of integration of Program:Gravatar msozeau2012-03-14
* Remove support for "abstract typing constraints" that requires unicity of sol...Gravatar msozeau2012-03-14
* Noise for nothingGravatar pboutill2012-03-02
* Corrects the erroneous error message when trying to unfocus a fullyGravatar aspiwack2012-03-01
* Removed a superfluous function in proof.mli. Preparing for incomingGravatar aspiwack2012-03-01
* Additional comment on Focus Conditions.Gravatar aspiwack2012-02-07
* A "Grab Existential Variables" to transform the unresolved evars at the end o...Gravatar aspiwack2012-02-07
* Typo in comments.Gravatar aspiwack2012-02-07
* Added an pattern / occurence syntax for vm_compute.Gravatar ppedrot2012-01-30
* Added documentation for "r foo" in Ltac debugger.Gravatar herbelin2012-01-20
* Breakpoints in Ltac debugger: new command "r foo" to jump to the nextGravatar herbelin2012-01-20
* Forbids (as it has always been the behaviour) to have two different openGravatar aspiwack2012-01-06
* 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
* Added a flag to control the use of typing when instantiating appliedGravatar herbelin2011-12-17
* Introducing a notion of evar candidates to be used when an evar isGravatar herbelin2011-12-16
* Proof using ...Gravatar gareuselesinge2011-12-12
* Added a DEPRECATED flag in declaration of options. For now only two options a...Gravatar ppedrot2011-11-24
* In emacs mode, prints a list of the dependent existential variables introducedGravatar aspiwack2011-11-23
* Fixing bug #2640 and variants of it (inconsistency between when andGravatar herbelin2011-11-17
* Bug 2636 - Move string_of_ppcmds to PpGravatar pboutill2011-11-14
* Add type annotations around all calls to Libobject.declare_objectGravatar letouzey2011-11-02
* Applying Tom Prince's patch to support parametric "constructor n" inGravatar herbelin2011-10-25
* Moved to a more standard order of arguments (i.e. env followed by evar_map)Gravatar herbelin2011-10-11
* Fixing Implicit Tactic mode damaged by commit r14496 (see also bug #2612).Gravatar herbelin2011-10-05
* Moving implicit tactic support from Tacinterp to Pfedit and final evarGravatar herbelin2011-09-26
* Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using the...Gravatar aspiwack2011-09-12
* Remove code concerning the obsolete Set/Unset UndoGravatar letouzey2011-09-05
* Porting Hendrik's 8.3 patch for proof tree visualization under proofGravatar herbelin2011-08-30
* Remove old file (1999)Gravatar msozeau2011-08-18
* Fixes mini-bug: Qed would succeed even on focused proofs.Gravatar aspiwack2011-08-12
* Propagated information from the reduction tactics to the kernel soGravatar herbelin2011-08-10
* Fixing typos in commentsGravatar herbelin2011-08-10
* Graceful error message for [Proof Mode] and [Set Default Proof Mode] when req...Gravatar aspiwack2011-08-10
* Stores bullet stack on locally at the level of focuses rather than globally i...Gravatar aspiwack2011-07-11
* Fixed bullets so that they would play well with { }.Gravatar aspiwack2011-07-06
* Extraction: forbid Prop-polymorphism of inductives when extracting to OcamlGravatar letouzey2011-07-04
* Cleaning debugging printer relative to new proof engine. InGravatar herbelin2011-06-21
* Generalizing flag use_evars_pattern_unification into a flagGravatar herbelin2011-06-18