aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* 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
* Univs: Fix bug #4363, nested abstract.Gravatar Matthieu Sozeau2015-12-11
* Document removal of Set Virtual Machine and -vm in CHANGES.Gravatar Maxime Dénès2015-12-11
* Remove Set Virtual Machine from doc, since the command itself has been removed.Gravatar Maxime Dénès2015-12-11
* Add tactic native_cast_no_check, analog to vm_cast_no_check.Gravatar Maxime Dénès2015-12-11
* Fixing a pat%constr bug. Thanks to Enrico for reporting.Gravatar Hugo Herbelin2015-12-10
* Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.Gravatar Hugo Herbelin2015-12-10
* Fixing compilation with OCaml 3.12 after commit 9d45d45f3a87 on removingGravatar Hugo Herbelin2015-12-10
* Silently ignore requests to _not_ clear something when that something cannot ...Gravatar Guillaume Melquiond2015-12-10
* Refman, ch. 4: A few fixes.Gravatar Hugo Herbelin2015-12-10
* ENH: redundant examples were removedGravatar Matej Kosik2015-12-10
* FIX: wrong reference to a figureGravatar Matej Kosik2015-12-10
* CLEANUP: putting examples inside "figure" environmentGravatar Matej Kosik2015-12-10
* ENH: The definition of the "_ ; _" operation on local context was added.Gravatar Matej Kosik2015-12-10
* TYPOGRAPHY: adjustmentsGravatar Matej Kosik2015-12-10
* PROPOSITION: the side-condition was made more specific.Gravatar Matej Kosik2015-12-10
* PROPOSITION: rephrasing of the explanation of the meaning of '[I:A|B]'Gravatar Matej Kosik2015-12-10
* PROPOSITION: Added an explicit definition of the notation for enriching the g...Gravatar Matej Kosik2015-12-10
* PROPOSITION: Added "if" and "then" words missing in the original sentence.Gravatar Matej Kosik2015-12-10
* PROPOSITION: Example was simplifiedGravatar Matej Kosik2015-12-10
* DONEGravatar Matej Kosik2015-12-10
* COMMENT: questionGravatar Matej Kosik2015-12-10
* COMMENT: questionGravatar Matej Kosik2015-12-10
* COMMENT: questionGravatar Matej Kosik2015-12-10
* COMMENT: questionGravatar Matej Kosik2015-12-10
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-12 14:00:08 +0000