aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Proof_global, STM: cleanup + use default_proof_mode instead of "Classic"Gravatar Enrico Tassi2016-05-10
| | | | | | | 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.
* STM: code cleanupGravatar Enrico Tassi2016-05-10
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-09
|\
| * Fix bug #3887: Better error message for "More than one program with unsolved ↵Gravatar Pierre-Marie Pédrot2016-05-09
| | | | | | | | obligations".
| * Rename Lexer -> CLexer.Gravatar Pierre-Marie Pédrot2016-05-09
| |
| * Fix typo in configure's option description.Gravatar Guillaume Melquiond2016-05-09
| |
| * Use "md5 -q" on FreeBSD architectures (bug #4719).Gravatar Guillaume Melquiond2016-05-09
| | | | | | | | | | | | 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.
| * Use the actual location of an error in the error pane (bug #4169).Gravatar Guillaume Melquiond2016-05-09
| | | | | | | | | | | | | | 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.
* | Exposing structure of the entries to tactic notation printers.Gravatar Pierre-Marie Pédrot2016-05-08
|\ \ | | | | | | | | | | | | This allows a proper printing of tactic notations with special tokens such as separators.
| * | Actually using the symbol information to print Tactic Notations properly.Gravatar Pierre-Marie Pédrot2016-05-08
| | |
| * | Removing dead code in Pptactic.Gravatar Pierre-Marie Pédrot2016-05-08
| | |
| * | Pass user symbol to tactic notation printers.Gravatar Pierre-Marie Pédrot2016-05-08
|/ /
* | Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
| |
* | Change the toplevel representation of Ltac values to an untyped one.Gravatar Pierre-Marie Pédrot2016-05-08
|\ \ | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | * Fix bug #4713: Anomaly: Assertion Failed for incorrect usage of Module.Gravatar Pierre-Marie Pédrot2016-05-08
| | |
| * | Normalizing the names of dynamic types to follow a typ_* scheme.Gravatar Pierre-Marie Pédrot2016-05-04
| | |
| | * typoGravatar Enrico Tassi2016-05-04
| | |
| | * NPeano : improve compatibility for this deprecated file via compat notationsGravatar Pierre Letouzey2016-05-04
| | |
| * | Removing useless generic arguments.Gravatar Pierre-Marie Pédrot2016-05-04
| | |
| * | Interpretation function can return any untyped value.Gravatar Pierre-Marie Pédrot2016-05-04
| | |
| * | Removing external uses of Val.inject and making Geninterp.interp return Val.tGravatar Pierre-Marie Pédrot2016-05-04
| | |
| * | Removing the Value.of_* API for parameterized types.Gravatar Pierre-Marie Pédrot2016-05-04
| | | | | | | | | | | | | | | Although still working, it is now bad practice to use it, and it is not widely spread anyway.
| * | Do not generate generic arguments for data which only requires toplevel values.Gravatar Pierre-Marie Pédrot2016-05-04
| | |
| * | More toplevel value representation sharing.Gravatar Pierre-Marie Pédrot2016-05-04
| | |
| * | Moving the Val module to Geninterp.Gravatar Pierre-Marie Pédrot2016-05-04
| | |
| * | Simplifying the code of Tacinterp.Gravatar Pierre-Marie Pédrot2016-05-04
| | |
| * | Getting rid of the Geninterp.generic_interp function.Gravatar Pierre-Marie Pédrot2016-05-04
| | |
| * | Switching to an untyped toplevel representation for Ltac values.Gravatar Pierre-Marie Pédrot2016-05-04
| | |
| * | Moving Ftactic and Geninterp to the engine folder.Gravatar Pierre-Marie Pédrot2016-05-04
|/ /
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-04
|\|
| * Int.v: simplify Jason's commit 5b4e3aceGravatar Pierre Letouzey2016-05-04
| |
| * Merge branch 'move-compat-notations' of https://github.com/JasonGross/coq ↵Gravatar Pierre Letouzey2016-05-04
| |\ | | | | | | | | | into v8.5
| * | Fixing subst.out after changing spacing in goal output (24a125b77).Gravatar Hugo Herbelin2016-05-04
| | |
| * | Fix Haskell extraction for terms over 45 characters longGravatar Nickolai Zeldovich2016-05-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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).
| * | Handle primitive projections inside types when extracting (bug #4616).Gravatar Guillaume Melquiond2016-05-04
| | | | | | | | | | | | | | | Note that extracting terms containing primitive projections is still utterly broken, so don't use them.
| * | Fix for #4603, part 3: definitions inside proofs not handled properly by coqc.Gravatar Maxime Dénès2016-05-04
| | | | | | | | | | | | Patch by Matthieu, Enrico and myself.
* | | Merge branch 'haskell-type-indent' of https://github.com/zeldovich/coq into ↵Gravatar Pierre Letouzey2016-05-04
|\ \ \ | | | | | | | | | | | | trunk
| | * | Increase the size of the dumpglob buffer for cooking notations (bug #4708).Gravatar Guillaume Melquiond2016-05-04
| | | | | | | | | | | | | | | | A single terminal character can take up to 5 bytes, e.g. "''^A'".
| | * | In Regular Subst Tactic mode, ensure that the order of hypotheses isGravatar Hugo Herbelin2016-05-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | * | Fix bug #4707: clearbody much slower in 8.5pl1.Gravatar Pierre-Marie Pédrot2016-05-03
| | | | | | | | | | | | | | | | | | | | We only retype hypotheses and conclusion when they do depend on the cleared identifier. This saves a lot of time.
| | * | Fix bug #3825: Universe annotations on notations should pass through or be ↵Gravatar Pierre-Marie Pédrot2016-05-03
| | | | | | | | | | | | | | | | rejected.
| | * | Test file for #4695: Slow Qed.Gravatar Maxime Dénès2016-05-03
| | | |
| | * | Fix bug #4292: Unexpected functor objects.Gravatar Pierre-Marie Pédrot2016-05-03
| | | |
| | * | Use the canonical name when looking for an eliminator (bug #4670).Gravatar Guillaume Melquiond2016-05-03
| | | | | | | | | | | | | | | | Disclaimer: I have no idea what I am doing.
* | | | A note concerning the "Drop" command.Gravatar Matej Kosik2016-05-03
| | | |
| | * | Fix bug #4705: coqtop accepts both -emacs and -ideslave.Gravatar Pierre-Marie Pédrot2016-05-03
| | | |
* | | | setup.txt : a guide explaining taming Emacs, Merlin, Company, Ocamldebug.Gravatar Matej Kosik2016-05-03
| | | |
| | * | Call hooks when terminating a definition proof (bug #4663).Gravatar Guillaume Melquiond2016-05-03
| | | | | | | | | | | | | | | | Also register properly the kind of definition.
| | * | Remove extraneous space in coqtop/pg output (bug #4675).Gravatar Guillaume Melquiond2016-05-03
| | | |
| | * | Make votour a bit more robust/forgiving with respect to user commands (bug ↵Gravatar Guillaume Melquiond2016-05-02
| | | | | | | | | | | | | | | | #4702).
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 12:24:25 +0000