aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Expand)AuthorAge
* still some more dead code removalGravatar letouzey2012-10-06
* remove Refiner.abstract_tactic and similarGravatar letouzey2012-10-06
* Clean-up : removal of Proof_type.tactic_exprGravatar letouzey2012-10-06
* Proof_type: rule now degenerates to prim_ruleGravatar letouzey2012-10-06
* Clean-up : no more Proof_type.proof_treeGravatar letouzey2012-10-06
* Clean-up of proof_type.ml : no more Nested nor abstract_tactic_boxGravatar letouzey2012-10-06
* Remove the unused "intel" field in Proof.proof_stateGravatar letouzey2012-10-02
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* Use the library function List.substract in prev commitGravatar letouzey2012-10-02
* Added a new tactical infoH tac, that displays the names of hypothesis created...Gravatar courtieu2012-10-01
* As r15801: putting everything from Util.array_* to CArray.*.Gravatar ppedrot2012-09-14
* Partial revert of Yann commit in order to use CLib.List when openingGravatar 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
* Reductionops refactoringGravatar pboutill2012-07-20
* Severe reorganisation of the code of tactics in Proofview.Gravatar aspiwack2012-07-11
* Small change in the printing of proofs for use by coqide.Gravatar aspiwack2012-07-10
* Change how the number of open goals is printed.Gravatar aspiwack2012-07-04
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* Forward-port fixes from 8.4 (15358, 15353, 15333).Gravatar msozeau2012-06-04
* Cleaning Pp.ppnl useGravatar ppedrot2012-06-01
* Getting rid of Pp.msgnl and Pp.message.Gravatar ppedrot2012-06-01
* Cancel the start of a proof if its init_tac fails (fix #2799)Gravatar letouzey2012-06-01
* Getting rid of Pp.msgGravatar ppedrot2012-05-30
* remove many excessive open Util & Errors in mli'sGravatar letouzey2012-05-29
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* Pattern as a mli-only file, operations in PatternopsGravatar letouzey2012-05-29
* New files intf/constrexpr.mli and intf/notation_term.mli out of TopconstrGravatar letouzey2012-05-29
* 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
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
* Evar_kinds.mli containing former Evd.hole_kind, avoid deps on EvdGravatar letouzey2012-05-29
* Pfedit: two superfluous openGravatar letouzey2012-05-29
* remove undocumented and scarcely-used tactic auto decompGravatar letouzey2012-04-23
* Two dead functions in Tacmach.Gravatar aspiwack2012-04-18
* 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