| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-05-11 | Thorough rewriting of the Pcoq API towards safety and static invariants. | Pierre-Marie Pédrot | |
| Amongst other things: 1. No more unsafe grammar extensions, except when going through the CAMLPX-based Pcoq.Gram module. This is mostly safe because CAMLPX adds casts to ensure that parsing rules are well-typed. In particular, constr notation is now based on GADTs ensuring well-typedness. 2. Less reliance on unsafe coq inside Pcoq, and exposing a self-contained API. The Entry module was also removed as it now results useless. 3. Purely functional API for synchronized grammar extension. This gets rid of quite buggy code maintaining a table of empty entries to work around CAMLPX bugs. The state modification is now explicit and grammar extensions synchronized with the summary must provide the rules they want to perform instead of doing so imperatively. | |||
| 2016-05-11 | The grammar_extend function now registers unsynchronized extensions. | Pierre-Marie Pédrot | |
| This made little sense, as all the uses of this function were actually called from toplevel ML modules. This was at best useless, and at worst a source of bugs when loading plugins and messing with backtracking. | |||
| 2016-05-11 | Making the grammar command extend API purely functional. | Pierre-Marie Pédrot | |
| Instead of leaving the responsibility of extending the grammar to the caller, we ask for a list of extensions in the return value of the function. | |||
| 2016-05-11 | Moving the constr empty entry registering to the state-based API. | Pierre-Marie Pédrot | |
| 2016-05-11 | Turning the grammar extend command API into a state-passing one. | Pierre-Marie Pédrot | |
| 2016-05-11 | Moving the grammar summary to Pcoq. | Pierre-Marie Pédrot | |
| 2016-05-10 | Delimiting the use of unsafe code in Pcoq. | Pierre-Marie Pédrot | |
| 2016-05-10 | Overlooked use of Gram instead of G module in Pcoq. | Pierre-Marie Pédrot | |
| This was probably wreaking havoc in tricky undo-redo scenarii. | |||
| 2016-05-10 | Further tidying of the constr extension code. | Pierre-Marie Pédrot | |
| 2016-05-10 | Type-safe constr notations. | Pierre-Marie Pédrot | |
| This removes the last call to unsafe_grammar_extend, so that all handwritten grammar extensions are now type-safe. Grammars defined by CAMLPX EXTEND are still using the unsafe interface, but as they insert explicit casts they are deemed safe. | |||
| 2016-05-10 | AlistNsep token now accepts an arbitrary separator. | Pierre-Marie Pédrot | |
| 2016-05-10 | Simpler data structure for Arules token. | Pierre-Marie Pédrot | |
| 2016-05-10 | Purer implementation of empty level registering in Pcoq. | Pierre-Marie Pédrot | |
| 2016-05-10 | Removing the Entry module now that rules need not be marshalled. | Pierre-Marie Pédrot | |
| 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). | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |