aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Fix a bug in the naming of binders.Gravatar Arnaud Spiwack2014-09-15
| | | 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.
* A small pass of code cleaning and clenv removing in Rewrite.Gravatar Pierre-Marie Pédrot2014-09-15
|
* Fixing bug #3619 in emacs mode.Gravatar Hugo Herbelin2014-09-15
|
* Avoid backtracking in typeclass search if a solution for a closedGravatar Matthieu Sozeau2014-09-15
| | | | | non-dependent or propositional constraint has already been found (same behavior as before previous patch).
* Fix bug #3610, allowing betaiotadelta reduction while unifying types ofGravatar Matthieu Sozeau2014-09-15
| | | | records in unification.ml.
* Fix bug #3621, using fold_left2 on arrays of the same size only.Gravatar Matthieu Sozeau2014-09-15
|
* Rework typeclass resolution and control of backtracking.Gravatar Matthieu Sozeau2014-09-15
| | | | | | | 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).
* Removing one Evd.merge in Rewrite.Gravatar Pierre-Marie Pédrot2014-09-15
|
* More invariants in Rewrite unification.Gravatar Pierre-Marie Pédrot2014-09-15
|
* The unifying functions of Rewrite uses the return types of strategies.Gravatar Pierre-Marie Pédrot2014-09-15
|
* Splitting the uses of the unification function according to the status ofGravatar Pierre-Marie Pédrot2014-09-15
| | | | the abs flag in rewrite.
* Rewrite.apply_strategy uses the same return type as strategies.Gravatar Pierre-Marie Pédrot2014-09-14
|
* Proper type for rewrite strategy results.Gravatar Pierre-Marie Pédrot2014-09-14
|
* Prepare goal name printing but no not print them at the current time.Gravatar Hugo Herbelin2014-09-13
|
* Using "Evd.restrict" in tactic clear so as to keep evar names.Gravatar Hugo Herbelin2014-09-13
|
* Exporting apply_subfilter from Evd.ml.Gravatar Hugo Herbelin2014-09-13
|
* Retroknowledge arguments are made VERNAC ARGUMENTS.Gravatar Pierre-Marie Pédrot2014-09-13
|
* Fixing synchronization of evar names table when merging evar_map.Gravatar Hugo Herbelin2014-09-13
|
* Providing a -type-in-type option for collapsing the universe hierarchy.Gravatar Hugo Herbelin2014-09-13
|
* Checking typability of evar instances. Using ";" to separate bindingsGravatar Hugo Herbelin2014-09-13
| | | | in instances.
* Fixing injection bug #3616 on sigma-types.Gravatar Hugo Herbelin2014-09-13
|
* While we don't have a clean alternative to Clenvtac, add a primitiveGravatar Matthieu Sozeau2014-09-12
| | | | for tclEVARS which might solve existing goals.
* Fix base_include due to change in argument order of env and evar_mapGravatar Matthieu Sozeau2014-09-12
|
* An old typo which was preventing example #3537 to work the same as itGravatar Hugo Herbelin2014-09-12
| | | | was working in 8.4.
* Add syntax [id]: to apply tactic to goal named id.Gravatar Hugo Herbelin2014-09-12
|
* Use evar name to print goal.Gravatar Hugo Herbelin2014-09-12
|
* Uniformisation of the order of arguments env and sigma.Gravatar Hugo Herbelin2014-09-12
|
* Parsing evar instances.Gravatar Hugo Herbelin2014-09-12
|
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
| | | | | instances still to do). Using heuristics to name after the quantifier name it comes. Also added a "sigma" to almost all printing functions.
* No plural for only one non existing focused goal.Gravatar Hugo Herbelin2014-09-12
|
* Fix source of initial goal.Gravatar Hugo Herbelin2014-09-12
|
* Commit 682aa67cc80 about enforcing that apply does not create newGravatar Hugo Herbelin2014-09-12
| | | | | evars was too liberal. Using an intermediate criterion which makes both tests apply.v and 3284.v working.
* Discontinued xml plugin: improve the README.Gravatar Arnaud Spiwack2014-09-12
| | | More information, less pmp.
* Replace the list of argument in tacexpr with a single row argument.Gravatar Arnaud Spiwack2014-09-12
| | | | | | 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.
* Oopps.. fixed the .ml not the .ml4Gravatar Matthieu Sozeau2014-09-11
|
* Use an AST for strategy names.Gravatar Matthieu Sozeau2014-09-11
|
* Fix test-suite files, and move some opened to closed.Gravatar Matthieu Sozeau2014-09-11
|
* Add a flag for restricting resolution of typeclasses toGravatar Matthieu Sozeau2014-09-11
| | | | | | | 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).
* Keeping a sub-optimal behavior of intros_possibly_replacing for ↵Gravatar Hugo Herbelin2014-09-11
| | | | compatibility with inversion
* Other bugs with "inversion as" (collision between user-provided names and ↵Gravatar Hugo Herbelin2014-09-11
| | | | generated equation names).
* Fix bug #3594: eta for constructors and functions at the same time whichGravatar Matthieu Sozeau2014-09-11
| | | | | was failing in this case due to the wrong postponment of an unsolvable ?X = RigidContext[?X] problem.
* Fix bug #3596, wrong treatment of projections in compute_constelim_direct.Gravatar Matthieu Sozeau2014-09-11
|
* Fix bug #3505.Gravatar Matthieu Sozeau2014-09-11
| | | | | | | 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).
* Fixing bug #3605.Gravatar Pierre-Marie Pédrot2014-09-11
|
* Removing remaining documentation of the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-11
|
* A step towards better differentiating when w_unify is used for subtermGravatar Hugo Herbelin2014-09-10
| | | | | | | | | | 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).
* Parsing and printing of primitive projections, fix buggy behavior whenGravatar Matthieu Sozeau2014-09-10
| | | | implicits do not allow to parse as an application and cleanup code.
* Fix generation of inductive elimination principle for primitive records.Gravatar Matthieu Sozeau2014-09-10
| | | | Let r.(p) be a strict subterm of r during the guardness check.
* Fix categorization of recursive inductives.Gravatar Matthieu Sozeau2014-09-10
|
* Fixing localisation of tactic errors (my mistake in himsg.ml essentially).Gravatar Hugo Herbelin2014-09-10
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-14 17:31:15 +0000