| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-09-13 | Checking typability of evar instances. Using ";" to separate bindings | Hugo Herbelin | |
| in instances. | |||
| 2014-09-13 | Fixing injection bug #3616 on sigma-types. | Hugo Herbelin | |
| 2014-09-12 | While we don't have a clean alternative to Clenvtac, add a primitive | Matthieu Sozeau | |
| for tclEVARS which might solve existing goals. | |||
| 2014-09-12 | Fix base_include due to change in argument order of env and evar_map | Matthieu Sozeau | |
| 2014-09-12 | An old typo which was preventing example #3537 to work the same as it | Hugo Herbelin | |
| was working in 8.4. | |||
| 2014-09-12 | Add syntax [id]: to apply tactic to goal named id. | Hugo Herbelin | |
| 2014-09-12 | Use evar name to print goal. | Hugo Herbelin | |
| 2014-09-12 | Uniformisation of the order of arguments env and sigma. | Hugo Herbelin | |
| 2014-09-12 | Parsing evar instances. | Hugo Herbelin | |
| 2014-09-12 | Referring to evars by names. Added a parser for evars (but parsing of | Hugo Herbelin | |
| instances still to do). Using heuristics to name after the quantifier name it comes. Also added a "sigma" to almost all printing functions. | |||
| 2014-09-12 | No plural for only one non existing focused goal. | Hugo Herbelin | |
| 2014-09-12 | Fix source of initial goal. | Hugo Herbelin | |
| 2014-09-12 | Commit 682aa67cc80 about enforcing that apply does not create new | Hugo Herbelin | |
| evars was too liberal. Using an intermediate criterion which makes both tests apply.v and 3284.v working. | |||
| 2014-09-12 | Discontinued xml plugin: improve the README. | Arnaud Spiwack | |
| More information, less pmp. | |||
| 2014-09-12 | Replace the list of argument in tacexpr with a single row argument. | Arnaud Spiwack | |
| This has several benefits * It replicates the "no quadrillion-uple" pattern at the level of types. Giving names to the various component will hopefully make for better error messages. * It is less typo-prone, as the whole row can be passed as an argument rather than retyping each of the arguments. Also makes for a terser [Tacexpr]. * More importantly: local changes to tactic expressions will more often be kept local. Which will avoid some extra tedious work, and make rebases on top of such changes significantly easier. | |||
| 2014-09-11 | Oopps.. fixed the .ml not the .ml4 | Matthieu Sozeau | |
| 2014-09-11 | Use an AST for strategy names. | Matthieu Sozeau | |
| 2014-09-11 | Fix test-suite files, and move some opened to closed. | Matthieu Sozeau | |
| 2014-09-11 | Add a flag for restricting resolution of typeclasses to | Matthieu Sozeau | |
| matching (i.e. no instanciation of the goal evars). Classes defined when [Set Typeclasses Strict Resolution] is on use the restricted resolution for all their instances (except for Hint Extern's). | |||
| 2014-09-11 | Keeping a sub-optimal behavior of intros_possibly_replacing for ↵ | Hugo Herbelin | |
| compatibility with inversion | |||
| 2014-09-11 | Other bugs with "inversion as" (collision between user-provided names and ↵ | Hugo Herbelin | |
| generated equation names). | |||
| 2014-09-11 | Fix bug #3594: eta for constructors and functions at the same time which | Matthieu Sozeau | |
| was failing in this case due to the wrong postponment of an unsolvable ?X = RigidContext[?X] problem. | |||
| 2014-09-11 | Fix bug #3596, wrong treatment of projections in compute_constelim_direct. | Matthieu Sozeau | |
| 2014-09-11 | Fix bug #3505. | Matthieu Sozeau | |
| When w_unifying primitive projection applications, force the unification of types of the projected records to recover instances for the parameters (evarconv does this automatically by unifying evar instances with their expected type). | |||
| 2014-09-11 | Fixing bug #3605. | Pierre-Marie Pédrot | |
| 2014-09-11 | Removing remaining documentation of the XML plugin. | Pierre-Marie Pédrot | |
| 2014-09-10 | A step towards better differentiating when w_unify is used for subterm | Hugo Herbelin | |
| selection (rewrite, destruct/induction, set or apply on scheme), for unification (apply on not a scheme, auto), the latter being separated into primary unification and unification for merging instances. No change of semantics from within Coq, if I did not mistake (but a function like secondOrderAbstraction does not set flags by itself anymore). | |||
| 2014-09-10 | Parsing and printing of primitive projections, fix buggy behavior when | Matthieu Sozeau | |
| implicits do not allow to parse as an application and cleanup code. | |||
| 2014-09-10 | Fix generation of inductive elimination principle for primitive records. | Matthieu Sozeau | |
| Let r.(p) be a strict subterm of r during the guardness check. | |||
| 2014-09-10 | Fix categorization of recursive inductives. | Matthieu Sozeau | |
| 2014-09-10 | Fixing localisation of tactic errors (my mistake in himsg.ml essentially). | Hugo Herbelin | |
| 2014-09-10 | More small bugs in intros_replacing. | Hugo Herbelin | |
| 2014-09-10 | Fixing inversion after having fixed intros_replacing | Hugo Herbelin | |
| in69665dd2480d364162933972de7ffa955eccab4d. There are still situations when "as" is not given where equations coming from injection are not yet removed, making invalid the computation of dependencies, what prevents an hypothesis to be cleared and replaced. | |||
| 2014-09-10 | Example for apply and evars. | Hugo Herbelin | |
| 2014-09-10 | Removing "eqn:" for "induction" in reference manual. | Hugo Herbelin | |
| 2014-09-10 | VernacExtend does not dispatch on type anymore. | Pierre-Marie Pédrot | |
| 2014-09-09 | - Fix printing and parsing of primitive projections, including the Set | Matthieu Sozeau | |
| Printing All cases (bug #3597). - Fix Ltac matching with primitive projections (bug #3598). - Spotted a problem with printing of constants with maximally implicit arguments due to strange "compatibility" interpretation of Arguments [X] as Arguments {X} but didn't fix it entirely yet (might cause incompatibilities). | |||
| 2014-09-09 | Merge remote-tracking branch 'jason/win32-improvements' into trunk | Enrico Tassi | |
| 2014-09-09 | Bump CoqSDK revision number | Jason Gross | |
| 2014-09-09 | Add a VERBOSE flag to make-sdk-win32 | Jason Gross | |
| For debugging purposes. | |||
| 2014-09-09 | Minor code style cleanup in make-sdk-win32 | Jason Gross | |
| 2014-09-09 | Support 64-bit cygwin | Jason Gross | |
| 2014-09-09 | Support machines that have a full or nonexistant C drive | Jason Gross | |
| 2014-09-09 | Support environments where `find` is Windows' find | Jason Gross | |
| 2014-09-09 | Displaying genarg tag in idtac. | Pierre-Marie Pédrot | |
| 2014-09-09 | Installer for win improved | Enrico Tassi | |
| - checks for paths containing whitespaces - Coqide has syntax highlighting - does not include the ocaml compiler, since it would not work anyway for the purpose of native compile. For that we really need the whole toolchain, including the C linker/assembler. Hence we should just recommend to install the SDK | |||
| 2014-09-09 | IDE: escape popup text (close: 3600) | Enrico Tassi | |
| 2014-09-09 | Load Prelude.vi if not Prelude.vo is found (Close: 3595) | Enrico Tassi | |
| 2014-09-09 | Marshalling errors should be bold and red (should never happen actually) | Enrico Tassi | |
| 2014-09-09 | A marshalling failure does not make a worker `Old | Enrico Tassi | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |