| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-05-17 | Removing the old refine tactic from the Tactics module. | Pierre-Marie Pédrot | |
| It is indeed confusing, as it has little to do with the proper refine defined in the New submodule. Legacy code relying on it should call the Logic or Tacmach modules instead. | |||
| 2016-05-17 | Put the "move" tactic in the monad. | Pierre-Marie Pédrot | |
| 2016-05-16 | Put the "change" tactic in the monad. | Pierre-Marie Pédrot | |
| 2016-05-16 | Put the "specialize_eq" tactic in the monad. | Pierre-Marie Pédrot | |
| 2016-05-16 | Put the "generalize dependent" tactic in the monad. | Pierre-Marie Pédrot | |
| 2016-05-16 | Put the "generalize" tactic in the monad. | Pierre-Marie Pédrot | |
| 2016-05-16 | Put the "cofix" tactic in the monad. | Pierre-Marie Pédrot | |
| 2016-05-16 | Put the "*_cast_no_check" tactics in the monad. | Pierre-Marie Pédrot | |
| 2016-05-16 | Put the "exact" family of tactic in the monad. | Pierre-Marie Pédrot | |
| 2016-05-16 | Put the "fix" tactic in the monad. | Pierre-Marie Pédrot | |
| 2016-05-16 | Put the "exact_constr" tactic in the monad. | Pierre-Marie Pédrot | |
| 2016-05-16 | Put the "clear" tactic into the monad. | Pierre-Marie Pédrot | |
| 2016-05-16 | Generate more user-readable tactic notation kernel names. | Pierre-Marie Pédrot | |
| This has no influence on user-side, and only makes the life of the debugging developer easier. | |||
| 2016-05-16 | Merge pull request #170 from relrod/patch-1 | Pierre-Marie Pédrot | |
| Fix a really small doc typo | |||
| 2016-05-15 | Fix a really small doc typo | Ricky Elrod | |
| 2016-05-14 | Hack in TACTIC EXTEND to maintain the 8.5 behaviour on badly designed arguments. | Pierre-Marie Pédrot | |
| Since TACTIC EXTEND relies on the usual tactic notation mechanism, the interpretation of an ML tactic first goes through a TacAlias node. This means that variables bound by the notation overwrite those of the current environment. It turns out to be problematic for badly designed arguments that close over variables of the environment, e.g. glob_constr, because the variables used at interpretation time are now different from the ones of parsing time. Ideally, those arguments should return a closure made of the inner argument together with the Ltac environment they were defined in. Unluckily, this would need some important changes in their design. Most notably, most of ssreflect ARGUMENT EXTEND actually create such closed arguments. In order to emulate the old behaviour, we rather use a hack by prefixing ML-bound variables by a character that is not accessible from user-side. | |||
| 2016-05-13 | Dyn: simplify API introducing an Easy submodule | Enrico Tassi | |
| Now the casual Dyn user does not need to be a GADT guru | |||
| 2016-05-13 | More informative error message when interpreting ltac variables in terms. | Pierre-Marie Pédrot | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |