| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 2014-08-01 | micromega : improve efficiency/termination of type-checking | Frédéric Besson | |
| * unused terms are generalised * proof is abstract | |||
| 2014-08-01 | Continuing (incomplete) cleaning of Inductiveops. | Hugo Herbelin | |
| 2014-08-01 | A tentative uniform naming policy in module Inductiveops. | Hugo Herbelin | |
| - realargs: refers either to the indices of an inductive, or to the proper args of a constructor - params: refers to parameters (which are common to inductive and constructors) - allargs = params + realargs - realdecls: refers to the defining context of indices or proper args of a constructor (it includes letins) - paramdecls: refers to the defining context of params (it includes letins) - alldecls = paramdecls + realdecls | |||
| 2014-08-01 | Removing more tactic compatibility layer. | Pierre-Marie Pédrot | |
| 2014-08-01 | Removing some tactic compatibility layer. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |