aboutsummaryrefslogtreecommitdiff
path: root/proofs
AgeCommit message (Expand)Author
2014-10-22Proofview: clean up code a little.Arnaud Spiwack
2014-10-22Proofview: move [list_goto] to the [CList] module.Arnaud Spiwack
2014-10-22Proofview: replace the functions iter_list and iter_list2 by generic monadic ...Arnaud Spiwack
2014-10-22Proofview: clean up commented out code.Arnaud Spiwack
2014-10-22Proofview: remove a redundant primitive.Arnaud Spiwack
2014-10-22Proofview: move more functions to the Unsafe module.Arnaud Spiwack
2014-10-22Proofview: split [V82] module into [Unsafe] and [V82].Arnaud Spiwack
2014-10-22Proofview.mli: no more reference to Goal.goal.Arnaud Spiwack
2014-10-22Proofview: factor init and dependent_init.Arnaud Spiwack
2014-10-22Remove unused functions for side effects.Arnaud Spiwack
2014-10-22Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.Arnaud Spiwack
2014-10-21Lazily check that an argument is dependent when constructing evar clauses.Pierre-Marie Pédrot
2014-10-21Adding an evar version of the make_clenv function.Pierre-Marie Pédrot
2014-10-16Revert "Naming main goal "Main""Hugo Herbelin
2014-10-16Refactoring proofview: make the definition of the logic monad polymorphic.Arnaud Spiwack
2014-10-16Grab Existential Variables: restore the goal order from v8.4.Arnaud Spiwack
2014-10-16Proofview: cleanup: no more reference to Goal.goal.Arnaud Spiwack
2014-10-16Put evars remaining after a tactic on the shelf.Arnaud Spiwack
2014-10-16Refine: proper scoping of the future goals.Arnaud Spiwack
2014-10-16Goal: remove [advance] from the API.Arnaud Spiwack
2014-10-16Proofview: remove unused [refresh_sigma] compatibility primitive.Arnaud Spiwack
2014-10-16Goal: remove some functions from the compatibility layer.Arnaud Spiwack
2014-10-16Goal: remove most of the API (make [Goal.goal] concrete).Arnaud Spiwack
2014-10-16Make [Goal.goal] be exactly [Evar.t].Arnaud Spiwack
2014-10-16Goal: remove dead code.Arnaud Spiwack
2014-10-16Expose Proofview.Refine.with_type in the API.Arnaud Spiwack
2014-10-16Proofview.Refine: remove the handle type, and simplify the API.Arnaud Spiwack
2014-10-16Move the handling of the principal evar from refine to evd.Arnaud Spiwack
2014-10-16Move the handling a new evars from the [Proofview.Refine] module to [Evd].Arnaud Spiwack
2014-10-16Proofview.Refine: delay the marking of new evars as goals from [new_evar] to ...Arnaud Spiwack
2014-10-16Proofview: small optimisation/simplification.Arnaud Spiwack
2014-10-13Add support for deactivating type class inference from induction/destruct.Hugo Herbelin
2014-10-13Adding a tactic which fails if one of the goals under focus is dependent in a...Hugo Herbelin
2014-10-13Naming main goal "Main"Hugo Herbelin
2014-10-09Added support for having one subgoal inheriting the name of its father in Ref...Hugo Herbelin
2014-10-09Removing Convert_concl and Convert_hyp from Logic.Hugo Herbelin
2014-10-09A version of convert_concl and convert_hyp in new proof engine.Hugo Herbelin
2014-10-06Make tclEFFECTS also update the env in the proof monadEnrico Tassi
2014-10-04A few Global.env removed.Hugo Herbelin
2014-10-01Factored out IDE goal structure.Carst Tankink
2014-09-30Add syntax for naming new goals in refine: writing ?[id] instead of _Hugo Herbelin
2014-09-29Merging some functions from evarutil.ml/evd.ml.Hugo Herbelin
2014-09-27Removing the last use of tclSENSITIVE in favour of tclNEWGOALS.Pierre-Marie Pédrot
2014-09-26Adding a tclNEWGOALS primitive.Pierre-Marie Pédrot
2014-09-18Fixing strange evarmap leak in goals.Pierre-Marie Pédrot
2014-09-17Be more conservative and keep the use of eq_constr in pretyping/ functions.Matthieu Sozeau
2014-09-17Fix bug #3593, making constr_eq and progress work up toMatthieu Sozeau
2014-09-17Revert "While resolving typeclass evars in clenv, touch only the ones that ap...Matthieu Sozeau
2014-09-17While resolving typeclass evars in clenv, touch only the ones that appear in theMatthieu Sozeau
2014-09-15Fix timing of evar-normalisation of goals in [Ftactic.nf_enter].Arnaud Spiwack
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-23 08:45:37 +0000