aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Expand)AuthorAge
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-06-01
|\
| * 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
* | Merge v8.5 into trunkGravatar Hugo Herbelin2015-05-15
|\|
| * Disable precompilation for native_compute by default.Gravatar Guillaume Melquiond2015-05-14
| * Safer typing primitives.Gravatar Pierre-Marie Pédrot2015-05-13
* | Exposing the minimal amount of internal of the Logic monad in order toGravatar Pierre-Marie Pédrot2015-05-06
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-05-05
|\|
| * 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
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-03-23
|\|
| * typoGravatar Enrico Tassi2015-03-22
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-03-11
|\|
| * admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Gravatar Enrico Tassi2015-03-11
* | Moving Proofview_monad to the engine/ folder.Gravatar Pierre-Marie Pédrot2015-02-28
* | Adding a new folder corresponding to the low-level part of the pretyperGravatar Pierre-Marie Pédrot2015-02-27
|/
* [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
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
* Make sure the goals on the shelve are identified as goal and unresolvable for...Gravatar Arnaud Spiwack2014-12-12
* An option SimplIsCbnGravatar Pierre Boutillier2014-12-12
* Extend the syntax of simpl with a delta flag.Gravatar Arnaud Spiwack2014-12-12
* Exporting store of goals so that new_evar in convert, intro, etc. canGravatar Hugo Herbelin2014-12-07
* Occur-check in refine.Gravatar Arnaud Spiwack2014-12-04
* Refine primitive: [unsafe] is now true by default.Gravatar Arnaud Spiwack2014-12-04
* Some refactoring following previous commit.Gravatar Arnaud Spiwack2014-12-04
* Better implementation of 4a858a51322f2dd488b02130ca82ebcc4dc9ca35.Gravatar Arnaud Spiwack2014-12-04
* Factoring 2ee213b824dda48c3fe60e95316daf09f07e8075.Gravatar Arnaud Spiwack2014-12-04
* Fixing bug #3682.Gravatar Pierre-Marie Pédrot2014-11-30
* Adding missing unsafe primitives to Proofview.Gravatar Pierre-Marie Pédrot2014-11-30
* Fix (somewhat obsolete) [Existential] command, which conflicted with the shelf.Gravatar Arnaud Spiwack2014-11-28