| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-08-05 | Experimentally adding an option for automatically erasing an | Hugo Herbelin | |
| hypothesis when using it in apply or rewrite (prefix ">", undocumented), and a modifier to explicitly keep it in induction or destruct (prefix "!", reminiscent of non-linerarity). Also added undocumented option "Set Default Clearing Used Hypotheses" which makes apply and rewrite default to erasing the hypothesis they use (if ever their argument is indeed an hypothesis of the context). | |||
| 2014-08-05 | Testing a replacement of "cut" by "enough" on a couple of test files. | Hugo Herbelin | |
| 2014-08-05 | Adding a syntax "enough" for the variant of "assert" with the order of | Hugo Herbelin | |
| subgoals and the role of the "by tac" clause swapped. | |||
| 2014-08-05 | A new step in the new "standard" naming policy for propositional hypotheses | Hugo Herbelin | |
| obtained from case analysis or induction. Made it under experimental status. This replaces commit bf7d2a3ad2535e7d57db79c17c81aaf67d956965 which was acting at the level of logic.ml. Now acting in tactics.ml. Parts of things to be done about naming (not related to Propositions): induction on H:nat+bool produces hypotheses n and b but destruct on H produces a and b. This is because induction takes the dependent scheme whose names are statically inferred to be a and b while destruct dynamically builds a new scheme. | |||
| 2014-08-05 | More proofs independent of the names generated by induction/elim over | Hugo Herbelin | |
| a dependent elimination principle for Prop arguments. | |||
| 2014-08-05 | Making references to Proof General and CoqIDE uniform in Reference Manual. | Hugo Herbelin | |
| 2014-08-05 | Chapter 4 of reference manual: Fixing asymmetric patterns error + | Hugo Herbelin | |
| no spacing in English before ":". | |||
| 2014-08-05 | Coqide: check_connection now also checks correct loading of coqide plugin + | Hugo Herbelin | |
| reports errors also from stderr. | |||
| 2014-08-05 | STM: new "par:" goal selector, like "all:" but in parallel | Enrico Tassi | |
| par: distributes the goals among a number of workers given by -async-proofs-tac-j (defaults to 2). | |||
| 2014-08-05 | STM: code restructured to reuse task queue for tactics | Enrico Tassi | |
| 2014-08-05 | Goal: API to get the solution of a goal | Enrico Tassi | |
| 2014-08-05 | make a few lines fit the screen | Enrico Tassi | |
| 2014-08-05 | STM: Classify Let as non asynchronous (Closes: #3486) | Enrico Tassi | |
| 2014-08-05 | Coqide: annoying popups with GTK errors only in debug mode | Enrico Tassi | |
| 2014-08-05 | Ring: prevent an error message to show in case of success. | Arnaud Spiwack | |
| Since [idtac] can, now, be used even if no goal is left, this error message which assumed that the goal was still open would run at every call of the [ring] tactic. Which lead to comically many nonsensical messages on the console during Coq's compilation. | |||
| 2014-08-05 | Documentation: a simple example for [numgoals]. | Arnaud Spiwack | |
| Now that [idtac] can print a single message for several goals, printing the number of goals is readable. | |||
| 2014-08-05 | Ltac's [idtac] is now interpreted outside of a goal if possible. | Arnaud Spiwack | |
| It avoids printing several times the same things when no constr are involved in the message. It also allows to print messages even after all goals have been solved. | |||
| 2014-08-05 | Ltac's idtac is now implemented using the new API. | Arnaud Spiwack | |
| 2014-08-05 | Tacinterp: [interp_message] and associate now only require an environment ↵ | Arnaud Spiwack | |
| rather than an entire goal. | |||
| 2014-08-05 | Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter]. | Arnaud Spiwack | |
| When "entering" in a goal, the environment observed by [tclENV] is changed (in the scope of the goal) to be that of the goal. I'm not entirely sure it is the right semantics. But it allows to write tactics which are agnostic of whether they are run in a goal or not. | |||
| 2014-08-05 | Documentation of [uconstr]: typesetting. | Arnaud Spiwack | |
| 2014-08-05 | Documentation: refine accept uconstr arguments. | Arnaud Spiwack | |
| 2014-08-05 | Doc: uconstr now has a tactic notation entry. | Arnaud Spiwack | |
| 2014-08-05 | Fix interpretation bug in [uconstr]. | Arnaud Spiwack | |
| Substitution of the Ltac variables would only occur if the internalised [uconstr] was of the form [glob, Some expr], which is the case only in tactics defined inside a proof, but not in tactics defined in [Ltac]. | |||
| 2014-08-05 | The [refine] tactic now accepts [uconstr]. | Arnaud Spiwack | |
| Arguments of refine can hence be built by tactics instead of given in their entirety in one go. | |||
| 2014-08-05 | Small refactoring: use [uconstr] instead of [constr] when relevant in ↵ | Arnaud Spiwack | |
| grammar rules. | |||
| 2014-08-05 | Properly declare uconstr as an argument for TACTIC EXTEND. | Arnaud Spiwack | |
| 2014-08-05 | Fix [uconstr] name for argextend. | Arnaud Spiwack | |
| 2014-08-05 | Better fix of e5c025 | Pierre Boutillier | |
| 2014-08-04 | One more optimization for guard checking of cofixpoints. | Maxime Dénès | |
| In check_one_cofix, we now avoid calling dest_subterms each time we meet a constructor by storing both the current tree (needed for the new criterion) and a precomputed array of trees for subterms. | |||
| 2014-08-04 | More optimization in guard checking. | Maxime Dénès | |
| When dynamically computing the recarg tree, we now prune it according to the inferred tree. Compilation of CompCert is now ok. | |||
| 2014-08-04 | Fix an exponential behavior in guard checker for cofixpoints. | Maxime Dénès | |
| I had introduced it by mistake due to my OCaml dyslexia :) Thanks to Enrico and Arnaud for saving my day! | |||
| 2014-08-04 | Fixing semantics of Univ.Level.equal. | Pierre-Marie Pédrot | |
| 2014-08-04 | STM: when looking up in the cache catch Expired exc | Carst Tankink | |
| 2014-08-04 | STM: generate Feedback message for parsing errors | Enrico Tassi | |
| 2014-08-04 | STM: use a real priority queue | Enrico Tassi | |
| 2014-08-04 | STM: encapsulate Pp.message in Feedback.feedback | Carst Tankink | |
| 2014-08-04 | STM: VtQuery holds the id of the state it refers to | Carst Tankink | |
| 2014-08-04 | Some comments in the interface of Proofview_monad. | Arnaud Spiwack | |
| 2014-08-04 | Cleaning the new implementation of the tactic monad continued. | Arnaud Spiwack | |
| Remove proofview_gen, which was the repository of the extracted code, and move it to proofview_monad, which has the actual interface used by the [Proofview] module to implement tactics. | |||
| 2014-08-04 | Cleaning of the new implementation of the tactic monad. | Arnaud Spiwack | |
| * Add comments in the code (mostly imported from Monad.v) * Inline duplicated module * Clean up some artifacts due to the extracted code. * [NonLogical.new_ref] -> [NonLogical.ref] (I don't even remember why I chose this name originally) * Remove the now superfluous [Proof_errors] module (which was used to define exceptions to be used in the extracted code). * Remove Monad.v | |||
| 2014-08-03 | Fix to make Coq compile, I think this should still be accepted. | Matthieu Sozeau | |
| 2014-08-03 | Fix infer conv using the wrong universe conversion flexibility information | Matthieu Sozeau | |
| for constants that are not unfolded during conversion. Fix discharge of polymorphic section variables over inductive types. | |||
| 2014-08-03 | - Fix handling of opaque polymorphic definitions which were turned transparent. | Matthieu Sozeau | |
| - Decomment code in reductionops forgotten after debugging. | |||
| 2014-08-03 | Move to a representation of universe polymorphic constants using indices for ↵ | Matthieu Sozeau | |
| variables. Simplifies instantiation of constants/inductives, requiring less allocation and Map.find's. Abstraction by variables is handled mostly inside the kernel but could be moved outside. | |||
| 2014-08-03 | - Fix has_undefined_evars not using its or_sorts argument anymore. | Matthieu Sozeau | |
| - Allow apply's unification to use conversion even if some polymorphic constants appear in the goal (consistent with occur_meta_or_evar, and evarconv in general). | |||
| 2014-08-03 | Chapter 4: Fixing ambiguity about whether the return predicate refers | Hugo Herbelin | |
| explicitly or implicitly to the variables in the as and in clauses + formatting. | |||
| 2014-08-03 | Fixing #3483 (graceful failing with notations to non-constructors in "match"). | Hugo Herbelin | |
| 2014-08-02 | Better struture for Ltac internalization environments in Constrintern. | Pierre-Marie Pédrot | |
| 2014-08-01 | Faster uconstr. | Arnaud Spiwack | |
| Detyping was called on every typed constr in the Ltac context which was costly as most of the context is likely not to be refered to in a particular uconstr. This commit calls detyping lazily instead. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |