aboutsummaryrefslogtreecommitdiff
path: root/proofs/proofview.ml
AgeCommit message (Expand)Author
2016-03-20Moving Proofview to pretyping/.Pierre-Marie Pédrot
2016-03-20Moving Refine to its proper module.Pierre-Marie Pédrot
2016-03-20Making Proofview independent of Logic.Pierre-Marie Pédrot
2016-03-20Making Proofview independent from Goal.Pierre-Marie Pédrot
2016-03-20Extruding the code for the Existential command from Proofview.Pierre-Marie Pédrot
2016-02-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-02-17Fixing the Proofview.Goal.goal function.Pierre-Marie Pédrot
2016-02-15merging conflicts with the original "trunk__CLEANUP__Context__2" branchMatej Kosik
2016-02-15Renaming functions in Typing to stick to the standard e_* scheme.Pierre-Marie Pédrot
2016-02-13Merge branch 'v8.5'Pierre-Marie Pédrot
2016-02-13Do not give a name to anonymous evars anymore. See bug #4547.Pierre-Marie Pédrot
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-02Use streams rather than strings to handle bullet suggestions.Guillaume Melquiond
2015-12-11Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-09The unshelve tactical now takes future goals into account.Pierre-Marie Pédrot
2015-12-09Adding an unshelve tactical.Pierre-Marie Pédrot
2015-11-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-12Fix bug #4412: [rewrite] (setoid_rewrite?) creates ill-typed terms.Pierre-Marie Pédrot
2015-11-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-02Made that the syntax [id]:tac also applies to the shelve, which is after all ...Hugo Herbelin
2015-10-29Removing the evar_map argument from s_enter.Pierre-Marie Pédrot
2015-10-20Proofview.Goal.sigma returns an indexed evarmap.Pierre-Marie Pédrot
2015-10-20Indexing Proofview.goals with a stage.Pierre-Marie Pédrot
2015-10-20Boxing the Goal.enter primitive into a record type.Pierre-Marie Pédrot
2015-10-20Renaming Goal.enter field into s_enter.Pierre-Marie Pédrot
2015-10-19Adding a monotonic variant of Goal.enter and Goal.nf_enter.Pierre-Marie Pédrot
2015-10-18Making Evarutil.new_evar monotonous.Pierre-Marie Pédrot
2015-10-18Constraining refine to monotonic functions.Pierre-Marie Pédrot
2015-07-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-07-27Slightly improving line break formatting in Info command.Hugo Herbelin
2015-05-06Exposing the minimal amount of internal of the Logic monad in order toPierre-Marie Pédrot
2015-04-22Tactical `progress` compares term up to potentially equalisable universes.Arnaud Spiwack
2015-02-24[Proofview.tclPROGRESS]: do not consider that trivial goal instantiation is p...Arnaud Spiwack
2015-02-23Fix some typos in comments.Guillaume Melquiond
2015-01-12Update headers.Maxime Dénès
2015-01-08Fixed and extend bullet related info/error messages. + doc.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-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-28Tactic primitives: missing [advance] lead to spurious dangling goals.Arnaud Spiwack
2014-11-22Exporting a primitive allowing to run completely the tactic monad.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:53:58 +0000