aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Extraction: msg_notice instead of msg_info.Gravatar Pierre Courtieu2016-01-04
* Fix handling of side-effects in case of `Opaque side-effects as well.Gravatar Matthieu Sozeau2016-01-04
* par: check if the goal is not ground and fail (fix #4465)Gravatar Enrico Tassi2016-01-04
* workers: purge short version of -load-vernac too (fix #4458)Gravatar Enrico Tassi2016-01-04
* Put implicits back as in 8.4.Gravatar Matthieu Sozeau2015-12-31
* Fix bug #4456, anomaly in handle-side effectsGravatar Matthieu Sozeau2015-12-31
* Do not dump a glob reference when its location is ghost. (Fix bug #4469)Gravatar Guillaume Melquiond2015-12-31
* Fixing bug #4462: unshelve: Anomaly: Uncaught exception Not_found.Gravatar Pierre-Marie Pédrot2015-12-29
* Inclusion of functors with restricted signature is now forbidden (fix #3746)Gravatar Pierre Letouzey2015-12-22
* (Partial) fix for bug #4453: raise an error instead of an anomaly.Gravatar Matthieu Sozeau2015-12-17
* spawn: fix leak of file descriptorsGravatar Enrico Tassi2015-12-17
* Updating credits.Gravatar Hugo Herbelin2015-12-16
* Update version numbers and magic numbers for 8.5rc1 release.Gravatar Maxime Dénès2015-12-16
* FIx parsing of tactic "simple refine".Gravatar Maxime Dénès2015-12-16
* Add a "simple refine" variant of "refine" that does not call "shelve_unifiable".Gravatar Guillaume Melquiond2015-12-16
* Extraction: slightly better heuristic for Obj.magic simplificationsGravatar Pierre Letouzey2015-12-16
* Extraction: fixed beta-red with Obj.magic (#2795 again) + other simplificationsGravatar Pierre Letouzey2015-12-16
* Proof using: do not clear unused section hyps automaticallyGravatar Enrico Tassi2015-12-15
* Fix test suite after change in extraction.Gravatar Maxime Dénès2015-12-15
* Extraction: more cautious use of intermediate result caching (fix #3923)Gravatar Pierre Letouzey2015-12-15
* Fix test-suite files after change in refine tactic.Gravatar Maxime Dénès2015-12-15
* Extraction: fix a few little glitches with my last commit (replacing unused v...Gravatar Pierre Letouzey2015-12-15
* Adding a test for the unshelve tactical.Gravatar Pierre-Marie Pédrot2015-12-15
* Refine tactic now shelves unifiable holes.Gravatar Pierre-Marie Pédrot2015-12-15
* Changing the order of the goals generated by unshelve.Gravatar Pierre-Marie Pédrot2015-12-15
* Extraction: replace unused variable names by _ in funs and matchs (fix #2842)Gravatar Pierre Letouzey2015-12-15
* Extraction: allow basic beta-reduction even through a MLmagic (fix #2795)Gravatar Pierre Letouzey2015-12-14
* Fixing little bug of coq_makefile with unterminated comment.Gravatar Hugo Herbelin2015-12-14
* extraction_impl.v: fix a typoGravatar Pierre Letouzey2015-12-14
* A test file for Extraction Implicit (including bugs #4243 and #4228)Gravatar Pierre Letouzey2015-12-14
* Extraction: propagate implicit args in inner fixpoint (bug #4243 part 2)Gravatar Pierre Letouzey2015-12-14
* Fix \label which was meants to be \ref in doc of CIC terms.Gravatar Maxime Dénès2015-12-14
* Remove a mention of Set Virtual Machine in doc.Gravatar Maxime Dénès2015-12-14
* CoqIDE: add 'you need to restart CoqIDE after changing shortcuts' messageGravatar Enrico Tassi2015-12-14
* Updating CHANGES with an incompatibility.Gravatar Hugo Herbelin2015-12-14
* Revert PMP's fix of #2498, which introduces an incompatibility with lablgtkGravatar Maxime Dénès2015-12-14
* Flag -compat 8.4 now loads Coq.Compat.Coq84.Gravatar Maxime Dénès2015-12-14
* Moved proof_admitted to its own file, named "AdmitAxiom.v".Gravatar Maxime Dénès2015-12-14
* Test file for #4363 was not complete.Gravatar Maxime Dénès2015-12-14
* Extraction: cosmetically avoid generating spaces on empty linesGravatar Pierre Letouzey2015-12-14
* Extraction: also get rid of explicit '\n' for haskellGravatar Pierre Letouzey2015-12-14
* Extraction: fix a pretty-print issueGravatar Pierre Letouzey2015-12-14
* Extraction: cleanup a hack (Pp.is_empty instead of Failure "empty phrase")Gravatar Pierre Letouzey2015-12-14
* Extraction: documentation of the new option Unset Extraction SafeImplicitsGravatar Pierre Letouzey2015-12-12
* Extraction: nicer implementation of ImplicitsGravatar Pierre Letouzey2015-12-12
* Extraction: check for remaining implicits after dead code removal (fix #4243)Gravatar Pierre Letouzey2015-12-12
* Extraction: fix for bug #4334 (use of delta_resolver in Extract_env)Gravatar Pierre Letouzey2015-12-12
* Extraction: avoid generating some blanks at end-of-lineGravatar Pierre Letouzey2015-12-12
* Indexing and documenting some options.Gravatar Pierre-Marie Pédrot2015-12-12
* Optimize occur_evar_upto_types, avoiding repeateadly looking into theGravatar Matthieu Sozeau2015-12-11
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 01:51:05 +0000