| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 2014-05-15 | Future: better error message | Enrico Tassi | |
| 2014-05-13 | Fix the behaviour of ML tactic notations w.r.t. Imports by making them | Pierre-Marie Pédrot | |
| substitutive. | |||
| 2014-05-13 | Test-suite for bug #3259. | Pierre-Marie Pédrot | |
| 2014-05-13 | Rewritten the sorting algorithm for universes with a better complexity. | Pierre-Marie Pédrot | |
| This should be now linear instead of the cubic Bellman-Ford algorithm. The new algorithm assumes that the universe graph is a DAG if we remove the {Le, Eq}-cycles, which is the case when the graph is consistent. Luckily we only use the sorting algorithm on such consistent graphs, in the Print Sorted Universes command. | |||
| 2014-05-12 | Update various polyproj bugs w.r.t. latest trunk | Jason Gross | |
| 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-12 | Moving the ML tactic extension mechanism to a Libobject-based one. | Pierre-Marie Pédrot | |
| 2014-05-12 | Plugin names must be declared in the header of .ml4 file, be they static or | Pierre-Marie Pédrot | |
| dynamic. This is done with the "DECLARE PLUGIN \"name\"" macro. | |||
| 2014-05-12 | Adding the possibility for ML modules to declare functions to be called at | Pierre-Marie Pédrot | |
| caching time, i.e. when the Declare ML Module command is evaluated. This can be used by both static and dynamic plugins. | |||
| 2014-05-12 | Fixing the undocumented -dumpgraphbox option of coqdep. | Pierre-Marie Pédrot | |
| 2014-05-11 | Using Maps to handle imports in Safe_typing. The order is irrelevant indeed, | Pierre-Marie Pédrot | |
| and the lookup operation proved to be costly when dealing with big libraries. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |