| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-06-18 | Proofs now take and return an evar_universe_context, simplifying interfaces | Matthieu Sozeau | |
| and avoiding explicit substitutions and merging of contexts, e.g. in obligations.ml. The context produced by typechecking a statement is passed in the proof, allowing the universe name context to be correctly folded as well. Mainly an API cleanup. | |||
| 2014-06-17 | Removing dead code. | Pierre-Marie Pédrot | |
| 2014-06-17 | Improve hotspot in Auto. | Pierre-Marie Pédrot | |
| 2014-06-13 | Check resolution of Metas turned into Evars by pose_all_metas_as_evars | Hugo Herbelin | |
| in unification.ml in case prefix 'e' of "apply" and co is not given. | |||
| 2014-06-12 | Passing some tactics to the new monad type. | Pierre-Marie Pédrot | |
| 2014-06-11 | Fix bug #3291, stack overflow in rewrite. | Matthieu Sozeau | |
| 2014-06-11 | Fix bug #3289 | Matthieu Sozeau | |
| 2014-06-11 | In generalized rewrite, avoid retyping completely and constantly the ↵ | Matthieu Sozeau | |
| conclusion, and results of unifying the lemma with subterms. Using Retyping.get_type_of instead results in 3x speedup in Ncring_polynom. | |||
| 2014-06-11 | fix handling of side effects in abstract (fixes QArithSternBrocot) | Enrico Tassi | |
| The right fix should probably be to remove the build_constant_by_tactic function and only use the build_by_tactic one | |||
| 2014-06-08 | Moving hook code from Future to Lemmas. This seemed to disrupt compilation of | Pierre-Marie Pédrot | |
| the checker, and it was not used before that anyway. | |||
| 2014-06-08 | Enforce a correct exception handling in declaration_hooks | Enrico Tassi | |
| This should finally get rid of the following class of bugs: Qed fails, STM undoes to the beginning of the proof because the exception is not annotated with the correct state, PG gets out of sync because errors always refer to the last command in PGIP. | |||
| 2014-06-07 | Adding a new Control file centralizing the control options of Coq. | Pierre-Marie Pédrot | |
| 2014-06-06 | Preserve compatibility on examples such as "intros []." on goals such | Hugo Herbelin | |
| as "forall x:nat*nat, x=x", which resulted in "forall n n0 : nat, (n, n0) = (n, n0)" before commit 37f68259ab0a33c3b5b41de70b08422d9bcd3bec on "Fixing introduction patterns * and ** ". | |||
| 2014-06-06 | Fixes the lost evars when interpreting a change with pattern tactic. | Arnaud Spiwack | |
| 2014-06-06 | Moving the [split] tactic out of the AST. | Pierre-Marie Pédrot | |
| 2014-06-04 | Collecting in Namegen those conventional default names that are used in ↵ | Hugo Herbelin | |
| different places | |||
| 2014-06-04 | - Fix hashing of levels to get the "right" order in universe contexts etc... | Matthieu Sozeau | |
| - Add a tentative syntax for specifying universes: Type{"i"} and foo@{Type{"i"},Type{"j"}}. These are always rigid. - Use level-to-level substitutions where the more general level-to-universe substitutions were previously used. | |||
| 2014-06-03 | The tactic interpreter now uses a new type of tactics, through | Pierre-Marie Pédrot | |
| the GTac module. A ['a Gtac.t] is a special case of tactic that may depend on the current goals, or not. Internally, it construct a list of results, one for each focussed goal, if the tactic is actually dependent. This allows for an interpretation of whole-goal tactic that does work, which was not the case for the previous implementation, which did to many Proofview.Goal.enter. | |||
| 2014-06-02 | Removing symmetry from the atomic tactics. | Pierre-Marie Pédrot | |
| 2014-05-31 | More on injection over a projectable "existT". - Fixing syntax "injection ↵ | Hugo Herbelin | |
| ... as ..." which was not working. - Now applying the simplification on any "existT" generated by "injection" (possible source of incompatibilities). | |||
| 2014-05-31 | Fixing introduction patterns * and ** when used in a branch so that they do ↵ | Hugo Herbelin | |
| not introduce beyond what is under control of the branch. See test-suite intros.v for an example. | |||
| 2014-05-31 | Upgrade Matthieu's new_revert as the "revert" (a "unit tactic"). | Hugo Herbelin | |
| 2014-05-27 | Removing a tclSENSITIVE from rewrite. | Pierre-Marie Pédrot | |
| 2014-05-26 | - Fix in kernel conversion not folding the universe constraints | Matthieu Sozeau | |
| correctly when comparing stacks. - Disallow Type i <= Prop/Set constraints, that would otherwise allow constraints that make a universe lower than Prop. - Fix stm/lemmas that was pushing constraints to the global context, it is done depending on the constant/variable polymorphic status now. - Adapt generalized rewriting in Type code to these fixes. | |||
| 2014-05-24 | Revert "Chasing the goal entering backward while interpreting tactics. This ↵ | Pierre-Marie Pédrot | |
| required" I tested the commit on the wrong branch... This reverts commit b0364eff4ec8ad5676060d8ca9cdbbb1d9c34d04. | |||
| 2014-05-24 | Chasing the goal entering backward while interpreting tactics. This required | Pierre-Marie Pédrot | |
| writing a new primitive recovering the first goal under focus. It sounds a bit hackish, but it does actually work. | |||
| 2014-05-22 | Moving the "specialize" tactic out of the AST. Also removed an obsolete | Pierre-Marie Pédrot | |
| variant of it, accepting an additional integer. | |||
| 2014-05-22 | Removing useless use of metaids in tactic AST. | Pierre-Marie Pédrot | |
| 2014-05-21 | Removing decompose record / sum from the tactic AST. | Pierre-Marie Pédrot | |
| 2014-05-21 | Allowing Ltac definitions that may be unusable because of a built-in | Pierre-Marie Pédrot | |
| parsing rule. | |||
| 2014-05-21 | Moving left & right tactics out of the AST. | Pierre-Marie Pédrot | |
| 2014-05-20 | Moving (e)transitivity out of the AST. | Pierre-Marie Pédrot | |
| 2014-05-20 | Tactics declared through TACTIC EXTEND that are of the form | Pierre-Marie Pédrot | |
| "foobar" constr(x1) ... constr(xn) are now defined as pure Ltac definitions, and do not add grammar nor printing rules. This partially relies on a hack consisting in retrieving the arguments in the tactic environment rather than as directly passed to the TacExtend node. | |||
| 2014-05-20 | Tentative to add constr-using primitive tactics without grammar rules. | Pierre-Marie Pédrot | |
| We eta-expand primitive Ltac functions, and instead of feeding TacExtend directly with its arguments, we use the environment to retrieve them. Some tactics from the AST were also moved away and made using this mechanism. | |||
| 2014-05-18 | When discrimination is not possible, try to project. | Maxime Dénès | |
| Example: Inductive Pnat : Prop := O | S : Pnat -> Pnat. Variable m n : Pnat. Goal S (S O) = S O -> False. intros H; injection H. now deduces S O = O instead of failing with an error message. | |||
| 2014-05-18 | Suggest Set Injection On Proofs in error message for injection. | Maxime Dénès | |
| 2014-05-18 | Restored old behavior of injection on proofs by default. | Maxime Dénès | |
| Use Set Injection On Proof to enable the new behavior. | |||
| 2014-05-16 | Moving argument-free tactics out of the AST into a dedicated | Pierre-Marie Pédrot | |
| "coretactics.ml4" file. | |||
| 2014-05-15 | poly: remove unused attribute to STM nodes and vernac classificaiton | Enrico Tassi | |
| 2014-05-12 | Now parsing rules of ML-declared tactics are only made available after the | Pierre-Marie Pédrot | |
| corresponding Declare ML Module command. This changes essentially two things: 1. ML plugins are forced to use the DECLARE PLUGIN statement before any TACTIC EXTEND statement. The plugin name must be exactly the string passed to the Declare ML Module command. 2. ML tactics are only made available after the Coq module that does the corresponding Declare ML Module is imported. This may break a few things, as it already broke quite some uses of omega in the stdlib. | |||
| 2014-05-09 | Code cleaning & factorizing functions in Equality. | Pierre-Marie Pédrot | |
| 2014-05-09 | Update and start testing rewrite-in-type code. | Matthieu Sozeau | |
| 2014-05-09 | Refresh universes for Ltac's type_of, as the term can be used anywhere, | Matthieu Sozeau | |
| fixing two opened bugs from HoTT/coq. | |||
| 2014-05-08 | Encapsulating some clausenv uses. This simplifies the control flow of some | Pierre-Marie Pédrot | |
| tactics. | |||
| 2014-05-08 | Revert "Avoid "revert" to retype-check the goal, and move it to a "new" tactic." | Hugo Herbelin | |
| (made push command with wrong local ref; leaving control to Matthieu on new revert) This reverts commit b797ba85b7b0f82d66af5629ccf6f75d90dda99a. | |||
| 2014-05-08 | Avoid "revert" to retype-check the goal, and move it to a "new" tactic. | Hugo Herbelin | |
| 2014-05-08 | Isolating a function "make_abstraction", new name of "letin_abstract", | Hugo Herbelin | |
| which compute an abstraction of the goal over a term or a pattern. | |||
| 2014-05-08 | Simplification and improvement of "subst x" in such a way that it | Hugo Herbelin | |
| works in the presence of local definitions referring to x and dependent in other hyps or concl. | |||
| 2014-05-08 | Renaming new_induct -> induction; new_destruct -> destruct. | Hugo Herbelin | |
| 2014-05-08 | Little reorganization of generalize tactics code w/o semantic changes. | Hugo Herbelin | |
| Also removing trailing spaces. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |