| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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-31 | Basic lemmas about the algebraic structure of equality. | Hugo Herbelin | |
| 2014-05-31 | Dead code + typo. | Hugo Herbelin | |
| 2014-05-30 | Adding test-suite for bug #3355. | Pierre-Marie Pédrot | |
| 2014-05-28 | - Fix for commit 15999903f875f4b5dbb3d5240d2ca39acc3cd777 which disallowed some | Matthieu Sozeau | |
| cases of Type (* Prop *) <= Set. - Do check types of metavariables at the end of apply's unification, if it failed at the beginning (otherwise universe constraints can be incomplete). | |||
| 2014-05-27 | Removing a tclSENSITIVE from rewrite. | Pierre-Marie Pédrot | |
| 2014-05-26 | Cbn reduces Pos.compare p~1 q~1 to Pos.compare p q | Pierre Boutillier | |
| (refolding of cbn is smarter) | |||
| 2014-05-26 | Reduction.Stack.Fix/Case stores Cst_stack.t | Pierre Boutillier | |
| 2014-05-26 | Cst_stack before stack (abstraction leak in whd_gen) | Pierre Boutillier | |
| 2014-05-26 | cbn: args list instead of arg number | Pierre Boutillier | |
| 2014-05-26 | Reductionops.Stack.map & Reduction.iterate_whd_gen | Pierre | |
| 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-26 | Update infer_conv to record trivial Prop <= Type i constraints that are ↵ | Matthieu Sozeau | |
| needed during unification. | |||
| 2014-05-26 | make coqdep canonicalize paths from the command line | Gregory Malecha | |
| - logical paths given to -R and -I should be split on periods. - it also seems like giving an empty string should result in the empty path rather than the singleton path with an empty string as an identifier. | |||
| 2014-05-26 | Fixing commit 9cef834. The parsing rules were generating an empty list, | Pierre-Marie Pédrot | |
| conflicting with the previous behaviour of 'eexists'. | |||
| 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-24 | Fixing TACTIC EXTEND for arguments-free tactics that may modify the whole | Pierre-Marie Pédrot | |
| proof. Indeed, computing an empty list of arguments triggered a Proofview.Goal.enter, which broke tactics like [shelve_unifiable]. This does not fix this particular tactic though, because the Ltac interpreter still enters the goal when calling a Ltac reference. | |||
| 2014-05-24 | Complying with reference manual for the syntax of exists/eexists, i.e. | Hugo Herbelin | |
| removing the strange kind of syntax "exists ,t,". which was equivalent to "split; exists t; split", as in e.g.: Goal (exists x, x=0) /\ (exists x, x=0). exists ,0,. Qed. This answers bug request #3340. | |||
| 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 | Fix native_compute for systems with a limited size for the command line. | Guillaume Melquiond | |
| The call to the native compiler can fail due to the sheer amounts of -I options passed to it. Indeed, it is easy to get the command line to exceed 512KB, thus causing various operating systems to reject it. This commit avoids the issue by only passing the -I options that matter for the currently compiled code. Note that, in the worst case, this commit is still not sufficient on Windows (32KB max), but this worst case should be rather uncommon and thus can be ignored for now. For the record, the command-line size mandated by Posix is 4KB. | |||
| 2014-05-22 | Ignore generated file. | Guillaume Melquiond | |
| 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 | Revert "Fix Qcanon after changes on injection." | Maxime Dénès | |
| This reverts commit f3b3b6e4d01080da4f0ce37a06553769e9588d0e. | |||
| 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-17 | Adding way to get the list of the accepted tactic notation arguments. | Pierre-Marie Pédrot | |
| 2014-05-17 | Fixing coqdep_boot warning relative to unknown ML files that were in tactics. | Pierre-Marie Pédrot | |
| 2014-05-17 | Fixing Camlp4 compilation | Pierre-Marie Pédrot | |
| 2014-05-16 | Revert "Decent error message when a constant is not found" | Enrico Tassi | |
| This reverts commit c4bdf93e358b97b32e0d80d6c7d1b79a2ece1dc2. | |||
| 2014-05-16 | More fixes of unification with primitive projections (missed cases during ↵ | Matthieu Sozeau | |
| the merge). Obligations are not necessarily opaque. | |||
| 2014-05-16 | Declare: fix Future management | Enrico Tassi | |
| 2014-05-16 | Decent error message when a constant is not found | Enrico Tassi | |
| 2014-05-16 | Fix unification of non-unfoldable primitive projections in evarconv. | Matthieu Sozeau | |
| 2014-05-16 | Moving argument-free tactics out of the AST into a dedicated | Pierre-Marie Pédrot | |
| "coretactics.ml4" file. | |||
| 2014-05-16 | Slightly better printer for native ML tactics, in order to disambiguate | Pierre-Marie Pédrot | |
| them. | |||
| 2014-05-16 | Tactics defined through TACTIC EXTEND that are only defined as a string do | Pierre-Marie Pédrot | |
| not create grammar and printing rules anymore, they define Ltac entries in the module that declares them instead. | |||
| 2014-05-16 | Another try at close_proof that should behave better w.r.t. exception handling. | Matthieu Sozeau | |
| 2014-05-15 | heads: avoid forcing opaque proofs | Enrico Tassi | |
| 2014-05-15 | poly: remove unused attribute to STM nodes and vernac classificaiton | Enrico Tassi | |
| 2014-05-15 | Polymorphic Lemmas are like Defined ones for STM | Enrico Tassi | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |