aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
* Fix bug #3591: print differently eta-expanded projection implicit ↵Gravatar Matthieu Sozeau2014-09-08
| | | | | | application and primitive projection when they would otherwise be ambiguous.
* Parsing of Type@{max(i,j)}.Gravatar Matthieu Sozeau2014-09-08
|
* Display number of available goals in "incorrect number of goals" error message.Gravatar Arnaud Spiwack2014-09-08
|
* CHANGES: existential variables are always "substituted" in the new tactic ↵Gravatar Arnaud Spiwack2014-09-08
| | | | engine.
* CHANGES: Ltac's [refine] accepts [uconstr].Gravatar Arnaud Spiwack2014-09-08
|
* Doc: [revgoals].Gravatar Arnaud Spiwack2014-09-08
|
* CHANGES: [revgoals].Gravatar Arnaud Spiwack2014-09-08
|
* Fix [induction] wrt inductive records and non-recursive variants.Gravatar Arnaud Spiwack2014-09-08
| | | | - [induction] on inductive records use the generated induction scheme for induction (not destruct as for non-recursive records) - [induction] on non-recursive variants do destruct as the induction scheme is not generated.
* CHANGES: [Variant], [Set Nonrecursive Elimination Schemes].Gravatar Arnaud Spiwack2014-09-08
|
* CHANGES: binder names from Ltac identifiers.Gravatar Arnaud Spiwack2014-09-08
|
* Rename [extract_ltac_uconstr_values] to [extract_ltac_constr_context].Gravatar Arnaud Spiwack2014-09-08
| | | The latter is more representative of its actual function: extract from the Ltac context the values which are relevant to the interpretation of terms (either type or untyped).
* The [constr:(…)] Ltac construction now shares the same context as ↵Gravatar Arnaud Spiwack2014-09-08
| | | | | | [uconstr:(…)]. - The binders names can be influenced by binders defined in Ltac (e.g. [let x:=fresh"y" in let u:=constr:(fun x:nat=>x) in idtac u] ). - Any untyped constr in the context can now be inserted and type-checked inside a constr. In particular, Gregory Malecha's original proposed syntax for type-checking untyped terms in Ltac is now available [let u:=uconstr:(I I) in let v := constr:(u) in idtac v].
* Add a tactic [revgoals] to reverse the list of focused goals.Gravatar Arnaud Spiwack2014-09-08
|
* Fix bug #3589, unification looping due to incorrect use of stack with ↵Gravatar Matthieu Sozeau2014-09-08
| | | | primitive projections.
* Little fix in documentation of inversion.Gravatar Hugo Herbelin2014-09-07
|
* Test for "inversion as" naming bug.Gravatar Hugo Herbelin2014-09-07
|
* A better check that an "as" clause has been given to inversion, soGravatar Hugo Herbelin2014-09-07
| | | | | | | that it clears things earlier in the "as" case, allowing intros_replacing to work without renaming the hypotheses. (clear_request was not a good idea here a priori, since its use was not related to the hypothesis to invert but to an hypothesis to inject).
* Fixing a bug in intros_replacing which was causing inversion notGravatar Hugo Herbelin2014-09-07
| | | | necessarily granting names given in the "as" clause.
* Fixing "simple inversion as" (bug #2164).Gravatar Hugo Herbelin2014-09-07
|
* Dead code in inv.ml.Gravatar Hugo Herbelin2014-09-07
|
* Regression test #3557Gravatar Hugo Herbelin2014-09-07
|
* Regression test for bug #2883.Gravatar Hugo Herbelin2014-09-07
|
* Fixing bug #3492.Gravatar Pierre-Marie Pédrot2014-09-07
|
* Inlining code in Tacinterp that was only used once.Gravatar Pierre-Marie Pédrot2014-09-06
|
* Code simplification in Tacinterp.Gravatar Pierre-Marie Pédrot2014-09-06
|
* Proper interpretation function for tauto.Gravatar Pierre-Marie Pédrot2014-09-06
| | | | | | | | | Instead of passing glob tactics through the infamous globTacticIn hack and antiquotation feature of the Ltac syntax, we put them in the interpretation environment as closures. This should be used everywhere to get rid of this buggy antiquotation syntax. This fixes bug #2800.
* Adding a way to inject tactic closures in interpretation values.Gravatar Pierre-Marie Pédrot2014-09-06
|
* Fixing clearbody : typecheck definitions in context.Gravatar Pierre-Marie Pédrot2014-09-06
|
* Renaming goal-entering functions.Gravatar Pierre-Marie Pédrot2014-09-06
| | | | | | | | | | | 1. Proofview.Goal.enter into Proofview.Goal.nf_enter. 2. Proofview.Goal.raw_enter into Proofview.Goal.enter. 3. Proofview.Goal.goals -> Proofview.Goals.nf_goals 4. Proofview.Goal.raw_goals -> Proofview.Goals.goals 5. Ftactic.goals -> Ftactic.nf_goals 6. Ftactic.raw_goals -> Ftactic.goals This is more uniform with the other functions of Coq.
* Fix bug #3584, elaborating pattern-matching on primitive records to theGravatar Matthieu Sozeau2014-09-06
| | | | use of projections.
* Remove debug printing codeGravatar Matthieu Sozeau2014-09-06
|
* Cleanup code for looking up projection bodies.Gravatar Matthieu Sozeau2014-09-06
|
* Fix checker to handle projections with eta and universe polymorphism correctly,Gravatar Matthieu Sozeau2014-09-06
| | | | simplifying conversion code.
* Fix checker to handle projections with eta and universe polymorphism correctly.Gravatar Matthieu Sozeau2014-09-06
|
* Fix checking of constants in checker. Prelude can now be checked.Gravatar Matthieu Sozeau2014-09-06
|
* Remove unused substitution functions in checker.Gravatar Matthieu Sozeau2014-09-05
|
* Fix checker treatment of inductives using subst_instances instead of ↵Gravatar Matthieu Sozeau2014-09-05
| | | | subst_univs_levels.
* Retype terms resulting from the feeding of a context with a term.Gravatar Pierre-Marie Pédrot2014-09-05
| | | | Fixes bug #3455.
* Fix checker/values.ml with latest changes due to projections and universes.Gravatar Matthieu Sozeau2014-09-05
|
* Remove a redundant typing phase in the [refine] tactic.Gravatar Arnaud Spiwack2014-09-05
| | | The refined term is still typechecked twice (not counting Qed). But there seem to be a bug in the typechecker whereby it sometimes return terms which have universe inconsistencies. Until this is fixed, I'll leave the second typing phase which seems to catch these inconsistencies. To remove it, it suffices to change the [unsafe] flag to [true].
* Silence an ocaml warning.Gravatar Arnaud Spiwack2014-09-05
|
* The pretyping of [uconstr] in [refine] uses the identifier of the ltac ↵Gravatar Arnaud Spiwack2014-09-05
| | | | context for goal contexts.
* Ltac's [uconstr] values now use the identifier context to give names to binders.Gravatar Arnaud Spiwack2014-09-05
| | | It does not work fine for refine yet as, while the binder has indeed the correct name, the evars are pretyped in an environment with the Ltac name, hence goal do not display the appropriate name.
* Adds an identifier context in pretying's Ltac context.Gravatar Arnaud Spiwack2014-09-05
| | | Binder names are interpreted as the Ltac specified one if available.
* Fix parsing of "subterm(s)" strategy argument.Gravatar Matthieu Sozeau2014-09-05
|
* Rename eta_expand_ind_stacks, fix the one from the checker and adaptGravatar Matthieu Sozeau2014-09-05
| | | | | it to the new representation of projections and the new mind_finite type.
* Adding a Ftactic module for potentially focussing tactics.Gravatar Pierre-Marie Pédrot2014-09-05
| | | | | | The code for the module was moved from Tacinterp. We still expose partially the implementation of the Ftactic.t type, for the sake of simplicity. It may be dangerous if used improperly though.
* Removing the old implementation of clear_body.Gravatar Pierre-Marie Pédrot2014-09-05
|
* Fix primitive projections declarations for inductive records.Gravatar Matthieu Sozeau2014-09-05
|
* At last a working clearbody!Gravatar Pierre-Marie Pédrot2014-09-05
| | | | | | | This time it should work at least as well as the previous version. The error messages were adapted a little. There is still a buggy behaviour when clearing lets in section, but this is mostly a problem of section handling. The v8.4 version of clearbody did exhibit the same behaviour anyway.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 16:15:16 +0000