| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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. | |||
| 2014-08-01 | CHANGES: [>…]. | Arnaud Spiwack | |
| 2014-08-01 | Document [> … ]. | Arnaud Spiwack | |
| 2014-08-01 | New tactical [> t1…tn] to apply tactics t1…tn to the corresponding goal. | Arnaud Spiwack | |
| Differs from the usual t;[t1…tn] in two ways: * It can be used without a preceding tactic * It counts every focused subgoal, rather than considering independently the goals generated by the application of the preceding tactic on individual goals. In other words t;[t1…tn] is [> t;[>t1…tn].. ]. | |||
| 2014-08-01 | Fix English spelling -> American spelling in doc. | Arnaud Spiwack | |
| 2014-08-01 | CHANGES: [numgoals] and [guard]. | Arnaud Spiwack | |
| 2014-08-01 | Document [numgoals] and [guard]. | Arnaud Spiwack | |
| 2014-08-01 | Add [guard] tactic. | Arnaud Spiwack | |
| The [guard] tactic accepts simple tests (on integers) as argument, succeeds if the test passes and fails if the test fails. Together with [numgoal] can be used to fork on the number of goals of a tactic. The syntax is not very robust (in particular [guard n<=1] is correct but not [guard (n<=1)]). Maybe tests should be moved to the general parser to allow for more flexibility. | |||
| 2014-08-01 | Add [numgoal] to Ltac. | Arnaud Spiwack | |
| 2014-08-01 | Add primtive [num_goal] to Proofview. | Arnaud Spiwack | |
| The [num_goal] tactic counts the number of focused goals. | |||
| 2014-08-01 | Untyped terms in ltac: simplify [coerce_to_uconstr]. | Arnaud Spiwack | |
| Following advice by Hugo Herbelin. | |||
| 2014-08-01 | Remove spurious [1] in equality.ml. | Arnaud Spiwack | |
| Introduced in a4043608f | |||
| 2014-08-01 | Clean outdated comment in Proofview.Notations. | Arnaud Spiwack | |
| 2014-08-01 | Fix typo in cf04daec997. | Arnaud Spiwack | |
| 2014-08-01 | micromega : vm_compute; reflexivity -> vm_cast_no_check (eq_refl true) | Frédéric Besson | |
| * Thanks to G. Melquiond for pointing out that 'abstract' already performs type-checking | |||
| 2014-08-01 | Compatibility for compilation with ocaml 3.12 (at least). | Hugo Herbelin | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |