aboutsummaryrefslogtreecommitdiff
path: root/proofs
AgeCommit message (Expand)Author
2015-07-29Fixing what seems to be a typo.Hugo Herbelin
2015-07-27Slightly improving line break formatting in Info command.Hugo Herbelin
2015-06-24Merge branch 'v8.5'Pierre-Marie Pédrot
2015-06-23Fix `Pp` function used by the `Info` command.Arnaud Spiwack
2015-06-22Merge remote-tracking branch 'forge/v8.5'Pierre Boutillier
2015-06-09STM: states coming from workers have no proof terminators (Close #4246)Enrico Tassi
2015-06-03Admitted does not drop poly-univ constraints (Fix #4244)Enrico Tassi
2015-06-01Merge branch 'v8.5'Pierre-Marie Pédrot
2015-05-29STM/Univ: save initial univs (the ones in the statement) in Proof.proofEnrico Tassi
2015-05-27Fix bug #4159Matthieu Sozeau
2015-05-18Tentative fix for #3461: Anomaly: Uncaught exception Pretype_errors.PretypeEr...Pierre-Marie Pédrot
2015-05-15Merge v8.5 into trunkHugo Herbelin
2015-05-14Disable precompilation for native_compute by default.Guillaume Melquiond
2015-05-13Safer typing primitives.Pierre-Marie Pédrot
2015-05-06Exposing the minimal amount of internal of the Logic monad in order toPierre-Marie Pédrot
2015-05-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-04-23Remove almost all the uses of string concatenation when building error messages.Guillaume Melquiond
2015-04-22Tactical `progress` compares term up to potentially equalisable universes.Arnaud Spiwack
2015-04-19Slightly more efficient implementation of the logic monad.Pierre-Marie Pédrot
2015-03-23Merge branch 'v8.5'Pierre-Marie Pédrot
2015-03-22typoEnrico Tassi
2015-03-11Merge branch 'v8.5'Pierre-Marie Pédrot
2015-03-11admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Enrico Tassi
2015-02-28Moving Proofview_monad to the engine/ folder.Pierre-Marie Pédrot
2015-02-27Adding a new folder corresponding to the low-level part of the pretyperPierre-Marie Pédrot
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-02-10Granting wish #4008.Pierre-Marie Pédrot
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-24Tentative workaround for bug #3798.Pierre-Marie Pédrot
2015-01-18Fix a big bug in native_compute tactic: since Hugo's 364decf59c, it wasMaxime Dénès
2015-01-12Update headers.Maxime Dénès
2015-01-08Avoiding introducing yet another convention in naming files.Hugo Herbelin
2015-01-08Fixed and extend bullet related info/error messages. + doc.Pierre Courtieu
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 11:16:33 +0000