| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-03-19 | Adding phantom types to discriminate normalized goals, and adding a way to | Pierre-Marie Pédrot | |
| observe non-normalized goals. | |||
| 2014-03-17 | Fix test-suite 2255.v | Pierre Boutillier | |
| 2014-03-07 | Useless tactic bindings in Tacticals. | Pierre-Marie Pédrot | |
| 2014-03-07 | Tentative fix for a very strange pervasive equality in Auto. | Pierre-Marie Pédrot | |
| 2014-03-07 | Fixing generic equality in Auto. | Pierre-Marie Pédrot | |
| 2014-03-05 | Remove some dead-code (thanks to ocaml warnings) | Pierre Letouzey | |
| The removed code isn't used locally and isn't exported in the signature | |||
| 2014-03-05 | Remove many superfluous 'open' indicated by ocamlc -w +33 | Pierre Letouzey | |
| With ocaml 4.01, the 'unused open' warning also checks the mli :-) Beware: some open are reported as useless when compiling with camlp5, but are necessary for compatibility with camlp4. These open are now marked with a comment. | |||
| 2014-03-03 | Fixing pervasive equalities. In particular, I removed the code that deleted | Pierre-Marie Pédrot | |
| duplicates in kernel side effects. They were chosen according to an equality that was quite irrelevant, and as expected this patch did not break the test-suite. | |||
| 2014-03-03 | Term dnets do no need to contain the afferent constr pattern in their nodes. | Pierre-Marie Pédrot | |
| 2014-03-03 | Removing Termdn, and putting the relevant code in Btermdn. The current Termdn | Pierre-Marie Pédrot | |
| file was useless and duplicated code from Btermdn itself. | |||
| 2014-03-03 | Extruding code not depending of the functor argument in Termdn. | Pierre-Marie Pédrot | |
| 2014-03-03 | Replacing arguments of Trie by a cancellable monoid. | Pierre-Marie Pédrot | |
| 2014-03-02 | Matching --> ConstrMatching (was clashing with OCaml's compiler-libs) | Pierre Letouzey | |
| There are currently two other clashs : Lexer and Errors, but for the moment these ones haven't impacted my experiments with extraction and compiler-libs, while this Matching issue had. And anyway the new name is more descriptive, in the spirit of the recent TacticMatching. | |||
| 2014-03-02 | Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code | Pierre Letouzey | |
| NB: new file miscprint.ml deserves to be part of printing.cma, but should be part of proofs.cma for the moment, due to use in logic.ml | |||
| 2014-03-01 | Fixing pervasive comparisons | Pierre-Marie Pédrot | |
| 2014-03-01 | Removing a fishy use of pervasive equality in Ltac backtrace printing. | Pierre-Marie Pédrot | |
| 2014-02-28 | Removing Pervasives.compare in Termdn. | Pierre-Marie Pédrot | |
| 2014-02-27 | Tacinterp: more refactoring. | Arnaud Spiwack | |
| Introducing List.fold_right and List.fold_left in Monad. | |||
| 2014-02-27 | Tacinterp: refactoring using Monad. | Arnaud Spiwack | |
| Adds a combinator List.map_right which chains effects from right to left. | |||
| 2014-02-27 | Code refactoring thanks to the new Monad module. | Arnaud Spiwack | |
| 2014-02-27 | Remove unsafe code (Obj.magic) in Tacinterp. | Arnaud Spiwack | |
| This commit also introduces a module Monad to generate monadic combinators (currently, only List.map). | |||
| 2014-02-27 | Proofview.Notations: Now that (>>=) is free, use it for tclBIND. | Arnaud Spiwack | |
| Impacts MapleMode. | |||
| 2014-02-27 | Get rid of the enterl/glist API for Proofview.Goal. | Arnaud Spiwack | |
| The prefered style is to use continuation passing style when necessary, or simply passing the goal explicitely in the case of interpretation functions which do not evolve the current goal. | |||
| 2014-02-27 | Tacinterp: yet another superfluous enterl. | Arnaud Spiwack | |
| 2014-02-27 | Tacinterp: spurious enterl. | Arnaud Spiwack | |
| This changes the tacinterp API, but only affects (one line of) the MapleMode contrib. | |||
| 2014-02-27 | Dead code: eval_ltac_constr. | Arnaud Spiwack | |
| 2014-02-25 | Tacinterp: remove the is_value check in Ltac's let-in. | Arnaud Spiwack | |
| It fixes micromega. It is frankly a mystery to me why psatz ever work. The semantics of Ltac's match is still fishy. | |||
| 2014-02-25 | Tacinterp: fewer enterl still. | Arnaud Spiwack | |
| 2014-02-25 | Tacinterp: fewer Proofview.Goal.enterl. | Arnaud Spiwack | |
| I'm trying to avoid unecessary construction of intermediate lists. Interpretation function don't modify the goals, they just need a goal in their context. Some care has to be given to the evar maps, though, as we can extract an outdated evar map from a goal (this is probably an undesirable feature, but significantly simplified the compatibility API). Also, Proofview.Goal.enter{,l} catch exceptions (and transfer the non-critical ones into errors of the tactics monad). So I had to do just that for every "enter" removed (I probably have been overprotective but it's better that way). Not as trivial a modification as it should, but it will hopefully go over well. It was much needed anyway. | |||
| 2014-02-25 | Tacinterp: clean up. | Arnaud Spiwack | |
| 2014-02-25 | Tacinterp: remove unnecessary return/bind pairs. | Arnaud Spiwack | |
| 2014-02-24 | TacticMatching: avoid some closure allocation in (<*>). | Arnaud Spiwack | |
| 2014-02-24 | Removed some trailing whitespaces. | Arnaud Spiwack | |
| 2014-02-24 | IStream: a concat_map primitive. | Arnaud Spiwack | |
| 2014-02-24 | A view type for IStream. | Arnaud Spiwack | |
| View types are better practice than option types for pattern-matching. (Plus, they save a minute amount of allocations) | |||
| 2014-02-16 | Removing non-marshallable data from the Agram constructor. Instead of | Pierre-Marie Pédrot | |
| containing opaque grammar objects, it now contains a string representing the entry. In order to recover the entry from the string, the former must have been created with [Pcoq.create_generic_entry] or similar. This is guaranteed for entries generated by ARGUMENT EXTEND, and must be done by hand otherwise. Some plugins were fixed accordingly. | |||
| 2014-02-04 | The constructor tactic now returns several successes. | Pierre-Marie Pédrot | |
| 2014-02-02 | Fixing bug #3226. | Pierre-Marie Pédrot | |
| 2014-01-31 | In Ltac's exact tactic: avoid checking the type of the term twice. | Arnaud Spiwack | |
| Following a remark by Jason Gross and Daniel Grayson. | |||
| 2014-01-28 | Fixing dependent inversion. Some exceptions were not caught by the tactic | Pierre-Marie Pédrot | |
| monad. | |||
| 2014-01-19 | Adding a default object to generic argument registering mechanism. | Pierre-Marie Pédrot | |
| 2014-01-17 | Fixing bug #1758: Print Hint output can be misleading if variable shadows ↵ | Pierre-Marie Pédrot | |
| hypothesis. | |||
| 2014-01-14 | Removing unused tactics in rewrite. | Pierre-Marie Pédrot | |
| 2014-01-10 | Exporting the full pretyper options in Goal.constr_of_raw. | Pierre-Marie Pédrot | |
| 2014-01-10 | Fix bug#2080: error message on Ltac name clash with primitive tactics | xclerc | |
| 2014-01-06 | Algebraized "No such hypothesis" errors | Pierre-Marie Pédrot | |
| 2014-01-04 | Code cleaning in Rewrite, may also result faster. | Pierre-Marie Pédrot | |
| 2013-12-24 | Qed: feedback when type checking is done | Enrico Tassi | |
| To make this possible the state id has to reach the kernel. Hence definition_entry has an extra field, and many files had to be fixed. | |||
| 2013-12-24 | Simplifying the use of hypinfos in Rewrite. | Pierre-Marie Pédrot | |
| 2013-12-23 | Rewrite.ml: removing direction flag from hypinfo. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |