aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
* Fixing interpretation of constr under binders which was broken afterGravatar Hugo Herbelin2014-10-02
| | | | | it became possible to have binding names themselves bound to ltac variables (2fcc458af16b).
* Fixing bug #2810 (autounfold on local variable declared as hint but cleared).Gravatar Hugo Herbelin2014-10-02
|
* Completing fixing order of parameters when translating fromGravatar Hugo Herbelin2014-10-02
| | | | | | | glob_constr to constr_pattern. Was partially fixed to solve #3088 (8e88b7adab) in but the order of lambdas was still incorrect as the fix of the order of lambdas in second-order pattern-matching for #3136 showed (83159124ce22).
* An evar name changed in output test.Gravatar Hugo Herbelin2014-10-02
|
* Adapting the output test Notations:Gravatar Hugo Herbelin2014-10-02
| | | | | | - unbound variables in notation are allowed, forcing only parsing mode - plus and mult are now themselves abbreviations - evars are named
* Added make dependency in %.out in output tests.Gravatar Hugo Herbelin2014-10-02
|
* Revert "test-suite: New names for vars but the expected invariant is preserved"Gravatar Hugo Herbelin2014-10-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | This reverts commit cc06ffe3df0ecc023ad046a085b0751ed4161cbf. Going back to the convention of naming bound variables in hypotheses of the goal as in 8.4. My arguments for the revert are: - apply ... with (id:=...) would have to be changed too, then possibly breaking the compatibility - the naming became dependent of the order of variables as in x:nat H:forall x0, x0=0 ===== goal but H:forall x, x=0 x:nat ===== goal Accordingly, this is all a matter of convention, since the meaning of bindings is anyway the same in both cases.
* Adapting output/Arguments_renaming.out after fixing printing ofGravatar Hugo Herbelin2014-10-02
| | | | | constants which without a @ would have a maximally inserted implicit argument.
* Print type and environment of unsolved holes.Gravatar Arnaud Spiwack2014-10-02
| | | | | | Was just printed in the case of internal holes. Also: replace [str] by [strbrk] in error message of unsolved holes for better layout.
* Work around issues with FO unification trying to unify terms ofGravatar Matthieu Sozeau2014-10-02
| | | | | | | | | potentially different types, resulting in ill-typed terms due to eta. Projection expansion now fails gracefully on retyping errors. The proper fix to unification, checking that the heads for FO have unifiable types, is currently too strong, adding unnecessary universe constraints, so it is disabled for now. It might be quite expensive too also it's not noticeable on the stdlib.
* Move eta-expansion after delta reduction in kernel reduction. This makesGravatar Matthieu Sozeau2014-10-02
| | | | | | it closer to evarconv/unification's behavior and it is less prone to weird failures and successes in case of first-order unification sending problems where the two terms have different types.
* Fix treatment of projections in Cst_stacks and unfolding behavior in evarconv.Gravatar Matthieu Sozeau2014-10-02
|
* eta contractionsGravatar Pierre Boutillier2014-10-01
|
* argument flip of Cyclic31.nshiftr and Cyclic31.nshiftlGravatar Pierre Boutillier2014-10-01
|
* Simpl less (so that cbn will not simpl too much)Gravatar Pierre Boutillier2014-10-01
|
* Fix cbn behavior wrt simpl no matchGravatar Pierre Boutillier2014-10-01
|
* Fix the refolding by cbn of mutal constants defined in not included modulesGravatar Pierre Boutillier2014-10-01
|
* Fixing nice printing of error reporting with ml tactics bound to ltac names.Gravatar Hugo Herbelin2014-10-01
|
* Made Tacsubst independent of Auto at linking time so that Tacenv doesGravatar Hugo Herbelin2014-10-01
| | | | not draw Auto.
* Going back on granting wish #1039 in f5d7b2b1e so that apply withGravatar Hugo Herbelin2014-10-01
| | | | | works correctly with an hypothesis of the context and knowing that related bug #3204 had its own fix.
* Fixing new failure of #3017 after 012fe1a96ba81ab (Referring to evarsGravatar Hugo Herbelin2014-10-01
| | | | | by names): VarInstance behaves like GoalEvar for type class resolution.
* Fixing use of arguments renaming in apply which was broken afterGravatar Hugo Herbelin2014-10-01
| | | | | reorganization of apply in d5fece25d8964d5d9fcd55b66164286aeef5fb9f: using renaming also in retyping.
* Updating to the new use of 3 universes, after Hurkens is simplified.Gravatar Hugo Herbelin2014-10-01
|
* STM: report the (structured) goals as XMLGravatar Carst Tankink2014-10-01
| | | | | The leafs of the XML trees are still pretty-printed strings, but this could be refined later on.
* Factored out IDE goal structure.Gravatar Carst Tankink2014-10-01
| | | | | | | | | | | | The more structured goal record type of CoqIDE is also useful for other interfaces (in particular, for PIDE). To support this, the datatype was factored out to the Proof module. In addition, the record gains a type parameter, to allow interfaces to adapt the output to their needs. To accommodate this type, the Proof module also gains the map_structured_proof that takes a Proof.proof and a function on the individual goals (in the context of an evar map) and produces a structured goal based on the goal transformer.
* Add additional location information to AST XMLs.Gravatar Carst Tankink2014-10-01
|
* coq_makefile: build and install *top.cmxs pluginsGravatar Enrico Tassi2014-10-01
| | | | | | | | These plugins, like coqidetop, stmworkertop and tacworkertop are intended for toploop replacements (see -toploop command line option). With this commit coq_makefile can be used as the build system for any user-interface-specific plugins.
* Removing test for bug #2080.Gravatar Pierre-Marie Pédrot2014-10-01
| | | | | Naming a Ltac definition like a built-in tactic used to fail, but now only spits out a warning. This is too complicated to test...
* Add a bunch of reproduction files for closed bugs.Gravatar Xavier Clerc2014-09-30
|
* Add a bunch of reproduction files for bugs.Gravatar Xavier Clerc2014-09-30
|
* Seeing IntroWildcard as an action intro pattern rather than as a naming patternGravatar Hugo Herbelin2014-09-30
| | | | | | | | | | (the action is "clear"). Added subst_intropattern which was missing since the introduction of ApplyOn intro patterns. Still to do: make "intros _ ?id" working without interferences when "id" is precisely the internal name used for hypotheses to discard.
* Add syntax for naming new goals in refine: writing ?[id] instead of _Gravatar Hugo Herbelin2014-09-30
| | | | | | | | will name the goal id; writing ?[?id] will use the first fresh name available based with prefix id. Tactics intro, rename, change, ... from logic.ml now preserve goal name; cut preserves goal name on its main premise.
* Simplify evarconv thanks to new delta status of projections,Gravatar Matthieu Sozeau2014-09-30
| | | | | using whd_state_gen to handle unfolding. Add an isProj/destProj in term. Use the proper environment everywhere in unification.ml.
* XML pretty printing for AST (work by François Poulain, project DoCoq)Gravatar Enrico Tassi2014-09-29
| | | | It is not 100% complete, but the main part is there.
* Notation: option to attach extra pretty printing rules to notationsGravatar Enrico Tassi2014-09-29
| | | | | | | | | | | so that one can retrieve them and pass them to third party tools (i.e. print the AST with the notations attached to the nodes concerned). Available syntax: - all in one: Notation "a /\ b" := ... (format "...", format "latex" "#1 \wedge #2"). - a posteriori: Format Notation "a /\ b" "latex" "#1 \wedge #2".
* CoqIDE: new message to print ASTGravatar Enrico Tassi2014-09-29
|
* typoGravatar Enrico Tassi2014-09-29
|
* do not explode if a plugin is not up to date on -help (Close: 3673)Gravatar Enrico Tassi2014-09-29
|
* Merging some functions from evarutil.ml/evd.ml.Gravatar Hugo Herbelin2014-09-29
| | | | | | | | | | | | | - Removed collect_evars which does not consider instance (use evars_of_term instead). - Also removed evars_of_evar_info which did not filter context (use evars_of_filterered_evar_info instead). This is consistent with printing goal contexts in the filtered way. Anyway, as of today, afaics goals filters are trivial because (if I interpret evarutil.ml correctly), evars with non-trivial filter necessarily occur in a conv pb. Conversely, conv pbs being solved when tactics are called, there should not be an evar used as a goal with a non-trivial filter.
* Printing evar instance in a more intuitive order.Gravatar Hugo Herbelin2014-09-29
|
* Restoring non-uniform delta on local and global constants in 2nd orderGravatar Hugo Herbelin2014-09-29
| | | | | unification for apply (compatibility reason). Waiting for another way to provide a more uniform scheme by default (keyed unification?).
* Documenting option -type-in-type.Gravatar Hugo Herbelin2014-09-29
|
* Adding a test for bug #2428.Gravatar Pierre-Marie Pédrot2014-09-29
|
* Bug fixed.Gravatar Matthieu Sozeau2014-09-29
|
* Fix test-suite filesGravatar Matthieu Sozeau2014-09-29
| | | | | 3566 gave a legitimate error, keyedrewrite was not setting keyed unification on.
* Fix printing of primitive record info.Gravatar Matthieu Sozeau2014-09-29
|
* In evarconv and unification, expand folded primitive projections toGravatar Matthieu Sozeau2014-09-29
| | | | | | | | | | their eta-expanded forms which can then unfold back to the unfolded primitive projection form. This removes all special code that was necessary to handle primitive projections before, while keeping compatibility. Also fix cbn which was not refolding primitive projections correctly in all cases. Update some test-suite files accordingly.
* Print information about primitive records (Print and About).Gravatar Matthieu Sozeau2014-09-28
|
* Keyed unification option, compiling the whole standard libraryGravatar Matthieu Sozeau2014-09-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | (but deactivated still). Set Keyed Unification to activate the option, which changes subterm selection to _always_ use full conversion _after_ finding a subterm whose head/key matches the key of the term we're looking for. This applies to rewrite and higher-order unification in apply/elim/destruct. Most proof scripts already abide by these semantics. For those that don't, it's usually only a matter of using: Declare Equivalent Keys f g. This make keyed unification consider f and g to match as keys. This takes care of most cases of abbreviations: typically Def foo := bar and rewriting with a bar-headed lhs in a goal mentioning foo works once they're set equivalent. For canonical structures, these hints should be automatically declared. For non-global-reference headed terms, the key is the constructor name (Sort, Prod...). Evars and metas are no keys. INCOMPATIBILITIES: In FMapFullAVL, a Function definition doesn't go through with keyed unification on.
* Index keys instead of simply global references.Gravatar Matthieu Sozeau2014-09-27
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 11:59:18 +0000