aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-05-10Cleaning old untested not any more interesting testing files.Hugo Herbelin
2017-05-09Merge PR#591: Add bmsherman/topology to the ciMaxime Dénès
2017-05-09Put .travis.yml in alphabetical orderJason Gross
2017-05-09Merge PR#619: Fix warnings in top_printersMaxime Dénès
2017-05-09Merge PR#612: Set Ltac Batch DebugMaxime Dénès
2017-05-09Merge PR#606: Added an option Set Debug CbvMaxime Dénès
2017-05-09Merge PR#621: Prevent user-defined ring morphisms from ever being evaluated.Maxime Dénès
2017-05-09Merge PR#615: coqtop -help: don't die if coqlib can't be foundMaxime Dénès
2017-05-09Merge PR#609: Fix bug #3659: -time should understand multibyte encodings.Maxime Dénès
2017-05-09Merge PR#617: [toplevel] Fix a couple of logical errors in error printing.Maxime Dénès
2017-05-09Prevent user-defined ring morphisms from ever being evaluated.Guillaume Melquiond
2017-05-08Fix warnings in top_printersGaetan Gilbert
Note that [@@@ocaml.warning "-32"] caused an error with Drop. It was put there because I didn't realise the warning was about a real issue.
2017-05-05[toplevel] Fix a couple of logical errors in error printing.Emilio Jesus Gallego Arias
In 4abb41d008fc754f21916dcac9cce49f2d04dd6d we switched back to use exceptions for error printing. However a couple of mistakes were present in that commit: - We wrongly absorbed the exception on `Vernac.compile`. However, it should be propagated as the caller will correctly print the error now. This introduced a critical bug as now `coqc` return the wrong exit status on error, breaking all sort of things. - We printed parsing exceptions twice; now it is not necessary to print the exception in the parsing handler as it will be propagated. I've checked this commit versus all previously reported bugs and it seems to work; we should definitively add a test-suite case to check that the exit code of `coqc` is correct, plus several other cases such as bugs https://coq.inria.fr/bugs/show_bug.cgi?id=5467 https://coq.inria.fr/bugs/show_bug.cgi?id=5485 https://coq.inria.fr/bugs/show_bug.cgi?id=5484 etc... See also PR #583
2017-05-05Remove dead code and unused open.Maxime Dénès
2017-05-05Merge PR#558: Adding a fold_glob_constr_with_binders combinatorMaxime Dénès
2017-05-05Remove two unused opens.Maxime Dénès
2017-05-05Merge PR#598: Removing dead code in Autorewrite.Maxime Dénès
2017-05-05Fix bug #3659: -time should understand multibyte encodings.Pierre-Marie Pédrot
We assume Coq always outputs UTF-8 (is it really the case?) and cut strings after 30 UTF-8 characters instead of using the standard String function.
2017-05-05Documenting Option.List.find.Hugo Herbelin
2017-05-05Cosmetic: unifying style within option.ml.Hugo Herbelin
2017-05-05Upgrading some local function as a general-purpose combinator Option.List.map.Hugo Herbelin
2017-05-05Adding a test-suite pattern-unification example that Econstr fixed.Hugo Herbelin
2017-05-05Merge PR#610: Improve documentation of assert / pose proof / specialize.Maxime Dénès
2017-05-05Merge PR#605: Report a useful error for dependent inductionMaxime Dénès
2017-05-05coqtop -help: don't die if coqlib can't be foundGaetan Gilbert
2017-05-05Merge PR#454: Printing unfocussed goals and toward a pg plugin.Maxime Dénès
2017-05-05Merge PR#593: Functional choice <-> [inhabited] and [forall] commuteMaxime Dénès
2017-05-05Remove unused open.Maxime Dénès
2017-05-05Merge PR#544: Anonymous universesMaxime Dénès
2017-05-05Adapted to EConstr.Pierre Courtieu
2017-05-04Adding an option "Set Ltac Batch Debug" to additionally run Ltac debug in ↵Hugo Herbelin
batch mode.
2017-05-04Improve documentation of assert / pose proof / specialize.Théo Zimmermann
This commits documents the as clause of specialize and that the as clause of pose proof is optional. It also mentions a feature of assert ( := ) that was available since 8.5 and was mentionned by @herbelin in: https://github.com/coq/coq/pull/248#issuecomment-297970503
2017-05-04Warning removed.Pierre Courtieu
2017-05-04labelizing argumentsPierre Courtieu
2017-05-04Adding an option "Printing Unfocused".Pierre Courtieu
Off by default. + small refactoring of emacs hacks in printer.ml.
2017-05-03Generalizing the tactic-in-term embedding to any generic argument.Pierre-Marie Pédrot
2017-05-03Generalizing the refine primitive so as to accept tactic arguments.Pierre-Marie Pédrot
2017-05-03Allowing to pass arbitrary data in internalization environments.Pierre-Marie Pédrot
2017-05-03Exporting Nametab generic API.Pierre-Marie Pédrot
2017-05-03FIx bug #5300: uncaught exception in "Print Assumptions".Cyprien Mangin
2017-05-03Merge PR#541: Fixing "decide equality" bug #5449Maxime Dénès
2017-05-03Merge PR#588: Allow interactive editing of {C,}Morphisms in PGMaxime Dénès
2017-05-03Merge PR#386: Better editing of the standard library in coqtop/PGMaxime Dénès
2017-05-03Make congruence reuse discriminate instead of rolling its own.Gaetan Gilbert
This changes the produced terms a bit, eg Axiom T : Type. Lemma foo : true = false -> T. Proof. congruence. Qed. used to produce fun H : true = false => let Heq := H : true = false in @eq_rect Type True (fun X : Type => X) I T (@f_equal bool Type (fun t : bool => if t then True else T) true false Heq) now produces fun H : true = false => let Heq : true = false := H in let H0 : False := @eq_ind bool true (fun e : bool => if e then True else False) I false Heq in False_rect T H0 i.e. instead of proving [True = T] by [f_equal] then transporting [I] across this identity, it now proves [False] by [eq_ind] then uses exfalso.
2017-05-03Merge PR#602: Fix more warningsMaxime Dénès
2017-05-03Merge PR#404: patch for printing types of let bindingsMaxime Dénès
2017-05-03Merge PR#603: Fix outdated description in RefMan.Maxime Dénès
2017-05-03Adding an even more compact mode for goal display.Pierre Courtieu
We want to print variables in vertical boxes as much as possible. The criterion to distinguish "variable" from "hypothesis" is not obvious. We chose this one but may change it in the future: X:T is a variable if T is not of type Prop AND T is "simple" which means T is either id or (t T1 .. Tn) Ti's are sort-typed (typicall Ti:Type, but not Ti:nat).
2017-05-03Added an option Set Debug Cbv.Hugo Herbelin
2017-05-03Report a useful error for dependent inductionTej Chajed
The dependent induction tactic notation is in the standard library but not loaded by default, leading to a parser error message that is confusing and unhelpful. This commit adds a notation for dependent induction to Init that fails and reports [Require Import Coq.Program.Equality.] is required to use [dependent induction].
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-28 05:35:10 +0000