| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-09-16 | More on printing references applied to implicit arguments. | Hugo Herbelin | |
| 2014-09-15 | Add a "Hint Mode ref (+ | -)*" hint for setting a global mode | Matthieu Sozeau | |
| of resulution for goals whose head is "ref". + means the argument is an input and shouldn't contain an evar, otherwise resolution fails. This generalizes the Typeclasses Strict Resolution option which prevents resolution to fire on underconstrained typeclass constraints, now the criterion can be applied to specific parameters. Also cleanup auto/eauto code, uncovering a potential backwards compatibility issue: in cases the goal contains existentials, we never use the discrimination net in auto/eauto. We should try to set this on once the contribs are stabilized (the stdlib goes through when the dnet is used in these cases). | |||
| 2014-09-15 | Adapting ltac output test to new interpretation of binders. | Hugo Herbelin | |
| 2014-09-15 | Fixing printing of @eq which was apparently wrong bug fixed by MS on Wed 10. | Hugo Herbelin | |
| 2014-09-15 | Not printing goal name (reinstalled by mistake in a previous commit). | Hugo Herbelin | |
| 2014-09-15 | Fixing line break in test for #3559. | Hugo Herbelin | |
| 2014-09-15 | Fix timing of evar-normalisation of goals in [Ftactic.nf_enter]. | Arnaud Spiwack | |
| All goals were normalised up front, rather than normalised after the tactic acting on previous goal had the chance to solve some evars, which then appeared non-instantiated to tactics which do not work up to evar map (most of them). | |||
| 2014-09-15 | Ltac names in binders: some Ltac values can be seen both as terms and ↵ | Arnaud Spiwack | |
| identifiers. Fixes Ergo. | |||
| 2014-09-15 | Fix: when interpreting a identifier in pretying, use the Ltac identifier ↵ | Arnaud Spiwack | |
| substitution at the right place. I used to change [id] to its interpretation before calling [pretype_id]. But it's incorrect: we need to use the Ltac interpretation only when looking up the rel context (where it has been interpreted previously). It would not be to use the interpreted identifier to look up the named context or the Ltac context. | |||
| 2014-09-15 | Fix a bug in the naming of binders. | Arnaud Spiwack | |
| The ident closure was not propagated when pretying a [uconstr] coming from a [uconstr] closure. This bug had never been reported, as far as I'm aware. | |||
| 2014-09-15 | A small pass of code cleaning and clenv removing in Rewrite. | Pierre-Marie Pédrot | |
| 2014-09-15 | Fixing bug #3619 in emacs mode. | Hugo Herbelin | |
| 2014-09-15 | Avoid backtracking in typeclass search if a solution for a closed | Matthieu Sozeau | |
| non-dependent or propositional constraint has already been found (same behavior as before previous patch). | |||
| 2014-09-15 | Fix bug #3610, allowing betaiotadelta reduction while unifying types of | Matthieu Sozeau | |
| records in unification.ml. | |||
| 2014-09-15 | Fix bug #3621, using fold_left2 on arrays of the same size only. | Matthieu Sozeau | |
| 2014-09-15 | Rework typeclass resolution and control of backtracking. | Matthieu Sozeau | |
| Add a global option to check for multiple solutions and fail in that case. Add another flag to declare classes as having unique instances (not checked but assumed correct, avoiding some backtracking). | |||
| 2014-09-15 | Removing one Evd.merge in Rewrite. | Pierre-Marie Pédrot | |
| 2014-09-15 | More invariants in Rewrite unification. | Pierre-Marie Pédrot | |
| 2014-09-15 | The unifying functions of Rewrite uses the return types of strategies. | Pierre-Marie Pédrot | |
| 2014-09-15 | Splitting the uses of the unification function according to the status of | Pierre-Marie Pédrot | |
| the abs flag in rewrite. | |||
| 2014-09-14 | Rewrite.apply_strategy uses the same return type as strategies. | Pierre-Marie Pédrot | |
| 2014-09-14 | Proper type for rewrite strategy results. | Pierre-Marie Pédrot | |
| 2014-09-13 | Prepare goal name printing but no not print them at the current time. | Hugo Herbelin | |
| 2014-09-13 | Using "Evd.restrict" in tactic clear so as to keep evar names. | Hugo Herbelin | |
| 2014-09-13 | Exporting apply_subfilter from Evd.ml. | Hugo Herbelin | |
| 2014-09-13 | Retroknowledge arguments are made VERNAC ARGUMENTS. | Pierre-Marie Pédrot | |
| 2014-09-13 | Fixing synchronization of evar names table when merging evar_map. | Hugo Herbelin | |
| 2014-09-13 | Providing a -type-in-type option for collapsing the universe hierarchy. | Hugo Herbelin | |
| 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. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |