| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-05-10 | Hardening the obsolete unsafe_grammar_statement API. | Pierre-Marie Pédrot | |
| 2016-05-10 | Removing dead code in Compat. | Pierre-Marie Pédrot | |
| 2016-05-10 | Proof_global, STM: cleanup + use default_proof_mode instead of "Classic" | Enrico Tassi | |
| The "Classic" string is still hard coded here in there in the system, but not in STM. BTW, the use of an hard coded "Classic" value suggests nobody really uses "Set Default Proof Mode" in .v files. | |||
| 2016-05-10 | STM: code cleanup | Enrico Tassi | |
| 2016-05-09 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-05-09 | Fix bug #3887: Better error message for "More than one program with unsolved ↵ | Pierre-Marie Pédrot | |
| obligations". | |||
| 2016-05-09 | Rename Lexer -> CLexer. | Pierre-Marie Pédrot | |
| 2016-05-09 | Fix typo in configure's option description. | Guillaume Melquiond | |
| 2016-05-09 | Use "md5 -q" on FreeBSD architectures (bug #4719). | Guillaume Melquiond | |
| This patch also disables the -makecmd option and the corresponding test, since the value is not stored for future use. This prevents gratuitously failing to configure on FreeBSD. | |||
| 2016-05-09 | Use the actual location of an error in the error pane (bug #4169). | Guillaume Melquiond | |
| A "sentence" includes all the blank lines and all the comments that precede a command. So its starting location might be far from any error it contains. This patch changes error reporting so that it relies on the location of errors rather than the location of erroneous sentences. | |||
| 2016-05-08 | Exposing structure of the entries to tactic notation printers. | Pierre-Marie Pédrot | |
| This allows a proper printing of tactic notations with special tokens such as separators. | |||
| 2016-05-08 | Actually using the symbol information to print Tactic Notations properly. | Pierre-Marie Pédrot | |
| 2016-05-08 | Removing dead code in Pptactic. | Pierre-Marie Pédrot | |
| 2016-05-08 | Pass user symbol to tactic notation printers. | Pierre-Marie Pédrot | |
| 2016-05-08 | Removing dead code and unused opens. | Pierre-Marie Pédrot | |
| 2016-05-08 | Change the toplevel representation of Ltac values to an untyped one. | Pierre-Marie Pédrot | |
| This brings the evaluation model of Ltac closer to those of usual languages, and further allows the integration of static typing in the long run. More precisely, toplevel constructed values such as lists and the like do not carry anymore the type of the underlying data they contain. This is mostly an API change, as it did not break any contrib outside of mathcomp. | |||
| 2016-05-08 | Fix bug #4713: Anomaly: Assertion Failed for incorrect usage of Module. | Pierre-Marie Pédrot | |
| 2016-05-04 | Normalizing the names of dynamic types to follow a typ_* scheme. | Pierre-Marie Pédrot | |
| 2016-05-04 | typo | Enrico Tassi | |
| 2016-05-04 | NPeano : improve compatibility for this deprecated file via compat notations | Pierre Letouzey | |
| 2016-05-04 | Removing useless generic arguments. | Pierre-Marie Pédrot | |
| 2016-05-04 | Interpretation function can return any untyped value. | Pierre-Marie Pédrot | |
| 2016-05-04 | Removing external uses of Val.inject and making Geninterp.interp return Val.t | Pierre-Marie Pédrot | |
| 2016-05-04 | Removing the Value.of_* API for parameterized types. | Pierre-Marie Pédrot | |
| Although still working, it is now bad practice to use it, and it is not widely spread anyway. | |||
| 2016-05-04 | Do not generate generic arguments for data which only requires toplevel values. | Pierre-Marie Pédrot | |
| 2016-05-04 | More toplevel value representation sharing. | Pierre-Marie Pédrot | |
| 2016-05-04 | Moving the Val module to Geninterp. | Pierre-Marie Pédrot | |
| 2016-05-04 | Simplifying the code of Tacinterp. | Pierre-Marie Pédrot | |
| 2016-05-04 | Getting rid of the Geninterp.generic_interp function. | Pierre-Marie Pédrot | |
| 2016-05-04 | Switching to an untyped toplevel representation for Ltac values. | Pierre-Marie Pédrot | |
| 2016-05-04 | Moving Ftactic and Geninterp to the engine folder. | Pierre-Marie Pédrot | |
| 2016-05-04 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-05-04 | Int.v: simplify Jason's commit 5b4e3ace | Pierre Letouzey | |
| 2016-05-04 | Merge branch 'move-compat-notations' of https://github.com/JasonGross/coq ↵ | Pierre Letouzey | |
| into v8.5 | |||
| 2016-05-04 | Fixing subst.out after changing spacing in goal output (24a125b77). | Hugo Herbelin | |
| 2016-05-04 | Fix Haskell extraction for terms over 45 characters long | Nickolai Zeldovich | |
| The Haskell extraction code would allow line-wrapping of the Haskell type definition, which would lead to unparseable Haskell code when the linebreak occured just before the type name. In particular, with a term name of 46 characters or more, the following Coq code: Definition xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx := tt. Extraction Language Haskell. Extraction xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx. would produce: xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx :: Unit xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx = Tt which failed to compile with GHC (according to Haskell's indentation rules, the "Unit" line must be indented to be treated as a continuation of the previous line). This patch always forces the type onto a separate line, and ensures that it is always indented by 2 spaces (just like the body of each definition). | |||
| 2016-05-04 | Handle primitive projections inside types when extracting (bug #4616). | Guillaume Melquiond | |
| Note that extracting terms containing primitive projections is still utterly broken, so don't use them. | |||
| 2016-05-04 | Fix for #4603, part 3: definitions inside proofs not handled properly by coqc. | Maxime Dénès | |
| Patch by Matthieu, Enrico and myself. | |||
| 2016-05-04 | Merge branch 'haskell-type-indent' of https://github.com/zeldovich/coq into ↵ | Pierre Letouzey | |
| trunk | |||
| 2016-05-04 | Increase the size of the dumpglob buffer for cooking notations (bug #4708). | Guillaume Melquiond | |
| A single terminal character can take up to 5 bytes, e.g. "''^A'". | |||
| 2016-05-03 | In Regular Subst Tactic mode, ensure that the order of hypotheses is | Hugo Herbelin | |
| preserved, which is a source of incompatibilities w.r.t. released 8.5 but which looks to me to be the only possible canonical behavior. This is I believe a better behavior than the Regular Subst Tactic behavior in the released 8.5 and 8.5pl1. There, the order of hypotheses in which substitutions happened was respected, but their interleaving with other hypotheses was not respected. So, I consider this to be a fix to the "Regular Subst Tactic" mode. Also added a more detailed "specification" of the "Regular" behavior of "subst" in the reference manual. | |||
| 2016-05-03 | Fix bug #4707: clearbody much slower in 8.5pl1. | Pierre-Marie Pédrot | |
| We only retype hypotheses and conclusion when they do depend on the cleared identifier. This saves a lot of time. | |||
| 2016-05-03 | Fix bug #3825: Universe annotations on notations should pass through or be ↵ | Pierre-Marie Pédrot | |
| rejected. | |||
| 2016-05-03 | Test file for #4695: Slow Qed. | Maxime Dénès | |
| 2016-05-03 | Fix bug #4292: Unexpected functor objects. | Pierre-Marie Pédrot | |
| 2016-05-03 | Use the canonical name when looking for an eliminator (bug #4670). | Guillaume Melquiond | |
| Disclaimer: I have no idea what I am doing. | |||
| 2016-05-03 | A note concerning the "Drop" command. | Matej Kosik | |
| 2016-05-03 | Fix bug #4705: coqtop accepts both -emacs and -ideslave. | Pierre-Marie Pédrot | |
| 2016-05-03 | setup.txt : a guide explaining taming Emacs, Merlin, Company, Ocamldebug. | Matej Kosik | |
| 2016-05-03 | Call hooks when terminating a definition proof (bug #4663). | Guillaume Melquiond | |
| Also register properly the kind of definition. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |