aboutsummaryrefslogtreecommitdiff
path: root/proofs
AgeCommit message (Expand)Author
2015-01-05Added more informative messages about bullets.Pierre Courtieu
2014-12-28Call nf_constraints also when compiling directly to voEnrico Tassi
2014-12-28Proof using: call "clear" to remove from sight the vars not selectedEnrico Tassi
2014-12-28remove debug prints (leftover)Enrico Tassi
2014-12-27proof_global: make it possible to call close_proof in a workerEnrico Tassi
2014-12-26Call Evd.nf_constraints only on Univ Poly constantsEnrico Tassi
2014-12-23Vi2vo: fix handling of univ constraints coming from the bodyEnrico Tassi
2014-12-19Better doc and a few fixes for Proof using.Enrico Tassi
2014-12-18Proof using: New vernacular to name sets of section variablesEnrico Tassi
2014-12-16msg_info now puts infomsg tag in emacs mode.Pierre Courtieu
2014-12-16Getting rid of Exninfo hacks.Pierre-Marie Pédrot
2014-12-12Make sure the goals on the shelve are identified as goal and unresolvable for...Arnaud Spiwack
2014-12-12An option SimplIsCbnPierre Boutillier
2014-12-12Extend the syntax of simpl with a delta flag.Arnaud Spiwack
2014-12-07Exporting store of goals so that new_evar in convert, intro, etc. canHugo Herbelin
2014-12-04Occur-check in refine.Arnaud Spiwack
2014-12-04Refine primitive: [unsafe] is now true by default.Arnaud Spiwack
2014-12-04Some refactoring following previous commit.Arnaud Spiwack
2014-12-04Better implementation of 4a858a51322f2dd488b02130ca82ebcc4dc9ca35.Arnaud Spiwack
2014-12-04Factoring 2ee213b824dda48c3fe60e95316daf09f07e8075.Arnaud Spiwack
2014-11-30Fixing bug #3682.Pierre-Marie Pédrot
2014-11-30Adding missing unsafe primitives to Proofview.Pierre-Marie Pédrot
2014-11-28Fix (somewhat obsolete) [Existential] command, which conflicted with the shelf.Arnaud Spiwack
2014-11-28Tactic primitives: missing [advance] lead to spurious dangling goals.Arnaud Spiwack
2014-11-23One more word about "simpl f": avoid "simpl f" to be printed "simpl f",Hugo Herbelin
2014-11-22Removing useless flag of the historical move tactic.Pierre-Marie Pédrot
2014-11-22Exporting a primitive allowing to run completely the tactic monad.Pierre-Marie Pédrot
2014-11-20Exporting the function handling side-effects only applied to terms.Pierre-Marie Pédrot
2014-11-16Enforcing a stronger difference between the two syntaxes "simplHugo Herbelin
2014-11-09new: Optimize Proof, Optimize HeapEnrico Tassi
2014-11-08Follow up to experimental eager evar unification in bcba6d1bc9:Hugo Herbelin
2014-11-07Removing the legacy intro tactic code.Pierre-Marie Pédrot
2014-11-04Removing the old rename tactic.Pierre-Marie Pédrot
2014-11-02Plural and singular forms in error messages.Hugo Herbelin
2014-11-01Info: do not record info trace unless needed.Arnaud Spiwack
2014-11-01Info: print a name for the primitive tactics in [Proofview].Arnaud Spiwack
2014-11-01Info: dispatching-branches are declared as such in the info trace.Arnaud Spiwack
2014-11-01Add [Info] command.Arnaud Spiwack
2014-11-01An API for info traces.Arnaud Spiwack
2014-10-27Cleaning and documenting Clenv.make_evar_clausePierre-Marie Pédrot
2014-10-25This commit introduces changes in induction and destruct.Hugo Herbelin
2014-10-25VarInstance are also goals.Hugo Herbelin
2014-10-24Change reduction_of_red_expr to return an e_reduction_function returningMatthieu Sozeau
2014-10-23Monad: change the error managing of two-list combinators.Arnaud Spiwack
2014-10-23Evd.future_goals: forgot to revert the list in two places.Arnaud Spiwack
2014-10-23Proofview: forgot to change an exception after refactoring in ( 9f51aafebd5f3...Arnaud Spiwack
2014-10-22Specializing tclBREAK so that it can choose the return exception in casePierre-Marie Pédrot
2014-10-22Oversight in ce260a0db279ce09dda70e079ae3c35b49f05ec4 (Proper scoping of futu...Arnaud Spiwack
2014-10-22Proofview: documentation and re-ordering.Arnaud Spiwack
2014-10-22Split [Proofview] into a file where the basic operations on the state are def...Arnaud Spiwack
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 04:25:10 +0000