aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Expand)AuthorAge
* Fixed (and changed) infoH.Gravatar Pierre Courtieu2015-10-21
* Categorizing debug messages as such + NonLogical uses loggers.Gravatar Pierre Courtieu2015-10-19
* Miscellaneous typos, spacing, US spelling in comments or variable names.Gravatar Hugo Herbelin2015-10-18
* Fix #4346 1/2: native casts were not inferring universe constraints.Gravatar Maxime Dénès2015-10-15
* Fix LemmaOverloadingGravatar Matthieu Sozeau2015-10-14
* Remove misleading warning (Close #4365)Gravatar Enrico Tassi2015-10-09
* Proof using: let-in policy, optional auto-clear, forward closure*Gravatar Enrico Tassi2015-10-08
* Fixing emacs output in debugging mode.Gravatar Pierre Courtieu2015-10-06
* Univs: fix handling of evd's universes and side effects in build_by_tacticGravatar Matthieu Sozeau2015-10-02
* Univs: fix handling of side effects/delayed proofsGravatar Matthieu Sozeau2015-10-02
* Changed status of Info messages from notice to info.Gravatar Pierre Courtieu2015-10-02
* Removing the generalization of the body of inductive schemes fromGravatar Hugo Herbelin2015-09-23
* Proof: suggest Admitted->Qed only if the proof is really complete (#4349)Gravatar Enrico Tassi2015-09-20
* Univs: Add universe binding lists to definitionsGravatar Matthieu Sozeau2015-09-14
* Reverting 16 last commits, committed mistakenly using the wrong push command.Gravatar Hugo Herbelin2015-08-02
* Removing the generalization of the body of inductive schemes fromGravatar Hugo Herbelin2015-08-02
* Fixing what seems to be a typo.Gravatar Hugo Herbelin2015-07-29
* Slightly improving line break formatting in Info command.Gravatar Hugo Herbelin2015-07-27
* Fix `Pp` function used by the `Info` command.Gravatar Arnaud Spiwack2015-06-23
* STM: states coming from workers have no proof terminators (Close #4246)Gravatar Enrico Tassi2015-06-09
* Admitted does not drop poly-univ constraints (Fix #4244)Gravatar Enrico Tassi2015-06-03
* STM/Univ: save initial univs (the ones in the statement) in Proof.proofGravatar Enrico Tassi2015-05-29
* Fix bug #4159Gravatar Matthieu Sozeau2015-05-27
* Tentative fix for #3461: Anomaly: Uncaught exception Pretype_errors.PretypeEr...Gravatar Pierre-Marie Pédrot2015-05-18
* Disable precompilation for native_compute by default.Gravatar Guillaume Melquiond2015-05-14
* Safer typing primitives.Gravatar Pierre-Marie Pédrot2015-05-13
* Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
* Tactical `progress` compares term up to potentially equalisable universes.Gravatar Arnaud Spiwack2015-04-22
* Slightly more efficient implementation of the logic monad.Gravatar Pierre-Marie Pédrot2015-04-19
* typoGravatar Enrico Tassi2015-03-22
* admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Gravatar Enrico Tassi2015-03-11
* [Proofview.tclPROGRESS]: do not consider that trivial goal instantiation is p...Gravatar Arnaud Spiwack2015-02-24
* Fix some typos in comments.Gravatar Guillaume Melquiond2015-02-23
* Granting wish #4008.Gravatar Pierre-Marie Pédrot2015-02-10
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Tentative workaround for bug #3798.Gravatar Pierre-Marie Pédrot2015-01-24
* Fix a big bug in native_compute tactic: since Hugo's 364decf59c, it wasGravatar Maxime Dénès2015-01-18
* Update headers.Gravatar Maxime Dénès2015-01-12
* Avoiding introducing yet another convention in naming files.Gravatar Hugo Herbelin2015-01-08
* Fixed and extend bullet related info/error messages. + doc.Gravatar Pierre Courtieu2015-01-08
* Added more informative messages about bullets.Gravatar Pierre Courtieu2015-01-05
* Call nf_constraints also when compiling directly to voGravatar Enrico Tassi2014-12-28
* Proof using: call "clear" to remove from sight the vars not selectedGravatar Enrico Tassi2014-12-28
* remove debug prints (leftover)Gravatar Enrico Tassi2014-12-28
* proof_global: make it possible to call close_proof in a workerGravatar Enrico Tassi2014-12-27
* Call Evd.nf_constraints only on Univ Poly constantsGravatar Enrico Tassi2014-12-26
* Vi2vo: fix handling of univ constraints coming from the bodyGravatar Enrico Tassi2014-12-23
* Better doc and a few fixes for Proof using.Gravatar Enrico Tassi2014-12-19
* Proof using: New vernacular to name sets of section variablesGravatar Enrico Tassi2014-12-18
* msg_info now puts infomsg tag in emacs mode.Gravatar Pierre Courtieu2014-12-16
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 19:31:13 +0000