| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-12-23 | A global [gfail] tactic which works like [fail] except that it fails even if ↵ | Arnaud Spiwack | |
| there is no focused goal. The 'g' is for "global". The arguments are the same as [fail]. Beware: [let x := constr:… in tac] is a goal-local operation regardless of whether [tac] is goal-local or not. | |||
| 2014-12-23 | Fix compilation error in some configurations. | Arnaud Spiwack | |
| This was due to the unqualified uses of "Lazy" being disambiguated in different manners. I just changed the constructor name to "Select". Fixes #3877. | |||
| 2014-12-19 | Add a backtracking version of Ltac's [match]. | Arnaud Spiwack | |
| [multimatch … with …] returns every possible successes: every matching branch and every successes of these matching branch, so that subsequent tactics can backtrack as well. | |||
| 2014-12-18 | Proof using: New vernacular to name sets of section variables | Enrico Tassi | |
| 2014-12-18 | Fixed bad newlines in output for std output and emacs. | Pierre Courtieu | |
| I added a emacs_logger. Still need to cleanup std_logger. | |||
| 2014-12-16 | msg_info now puts infomsg tag in emacs mode. | Pierre Courtieu | |
| Fixes the idtac "string" not appearing in proofgeneral because printined *before* the goal. | |||
| 2014-12-15 | Changed bullet informations to warning for better display in PG. | Pierre Courtieu | |
| Since it displays together with the goal, it is better (for pg and other interfaces probably) that they are in a different message. | |||
| 2014-12-15 | About now accepts hypothesis names and goal selector. | Pierre Courtieu | |
| 2014-12-12 | Add Ltac syntax for the [tclIFCATCH] primitive. | Arnaud Spiwack | |
| [tryif t then t2 else t3] behaves like [t;t2] if [t] has at least one success, or [t3] otherwise. It generalises [t||t3] as failures from [t2] will not be caught. | |||
| 2014-12-12 | Extend the syntax of simpl with a delta flag. | Arnaud Spiwack | |
| You can write 'simpl -[plus minus] div2'. Simpl does not use it for now. | |||
| 2014-12-12 | Searchxxx now search also the hypothesis and support goal selector. | Pierre Courtieu | |
| Documentation also updated. | |||
| 2014-12-04 | Improving error message when one instance-hole is not found. | Hugo Herbelin | |
| Still to do: - Decide between using SeveralInstancesFound or raising an error when multiple instances exist. - Use a proper printer for evars instead of the debugging pr_evar_map_filter printer in pr_constraints. | |||
| 2014-11-30 | Fixing printing of dirpathes in Ppconstr. It was reversed. | Pierre-Marie Pédrot | |
| 2014-11-25 | Adding tag output to references in Ppconstr. | Pierre-Marie Pédrot | |
| 2014-11-24 | Plugging console highlighting in for toplevel and compilation error messages. | Pierre-Marie Pédrot | |
| 2014-11-22 | Removing useless flag of the historical move tactic. | Pierre-Marie Pédrot | |
| 2014-11-20 | Setting printing flags on the printing of mutual inductives. | Pierre-Marie Pédrot | |
| 2014-11-20 | Moving mutual inductive printing from Printer to Printmod. | Pierre-Marie Pédrot | |
| 2014-11-19 | Print [uconstr] in genargs. | Arnaud Spiwack | |
| 2014-11-19 | Proper printer for [uconstr] in [Pptactic]. | Arnaud Spiwack | |
| This particular instance is probably never called though. | |||
| 2014-11-19 | Printing function for [uconstr]. | Arnaud Spiwack | |
| The core is a "detyping" function for [closed_glob_constr]. Which interpretes the variable names according to the Ltac context, and apply the standard detyping procedure to typed terms in the closure. | |||
| 2014-11-19 | Adding rich-printing facilities to Printmod. | Pierre-Marie Pédrot | |
| 2014-11-17 | Adding notation terminals to coqtop highlight. | Pierre-Marie Pédrot | |
| 2014-11-17 | Fixing semantics of Ppconstr.print_hunks. | Pierre-Marie Pédrot | |
| 2014-11-17 | Missing keywords in Ppconstr. | Pierre-Marie Pédrot | |
| 2014-11-17 | Setting printing tags for Ltac. | Pierre-Marie Pédrot | |
| 2014-11-17 | Moving printing code for red_expr and may_eval to Pptactic. | Pierre-Marie Pédrot | |
| 2014-11-17 | Default styles for printing tags. | Pierre-Marie Pédrot | |
| They should be rather sensible, but de gustibus & coloribus... | |||
| 2014-11-17 | Setting error tag on generic errors returned by Coqtop. | Pierre-Marie Pédrot | |
| 2014-11-16 | Enforcing a stronger difference between the two syntaxes "simpl | Hugo Herbelin | |
| reference" and "simpl pattern" in the code (maybe we should have merged them instead, but I finally decided to enforce their difference, even if some compatibility is to be preversed - the idea is that at some time "simpl reference" would only call a weak-head simpl (or eventually cbn), leading e.g. to reduce 2+n into S(1+n) rather than S(S(n)) which could be useful for better using induction hypotheses. In the process we also implement the following: - 'simpl "+"' is accepted to reduce all applicative subterms whose head symbol is written "+" (in the toplevel scope); idem for vm_compute and native_compute - 'simpl reference' works even if reference has maximally inserted implicit arguments (this solves the "simpl fst" incompatibility) - compatibility of ltac expressions referring to vm_compute and native_compute with functor application should now work (i.e. vm_compute and native_compute are now taken into account in tacsubst.ml) - for compatibility, "simpl eq" (assuming no maximal implicit args in eq) or "simpl @eq" to mean "simpl (eq _ _)" are still allowed. By the way, is "mul" on nat defined optimally? "3*n" simplifies to "n+(n+(n+0))". Are there some advantages of this compared to have it simplified to "n+n+n" (i.e. to "(n+n)+n"). | |||
| 2014-11-15 | Adding tags to messages. | Pierre-Marie Pédrot | |
| 2014-11-15 | Additional style tags for constrs. | Pierre-Marie Pédrot | |
| 2014-11-15 | Setting a keyword tag in Ppconstr. | Pierre-Marie Pédrot | |
| 2014-11-15 | Adding a pretty-printing style library. | Pierre-Marie Pédrot | |
| 2014-11-13 | Move conjugate_verb_to_be next to cString.plural. | Hugo Herbelin | |
| 2014-11-10 | Plug the dynamic tags in the Richpp mechanism. | Pierre-Marie Pédrot | |
| 2014-11-09 | Removing a unused boolean in the TacMove node of tacexpr AST. | Pierre-Marie Pédrot | |
| 2014-11-07 | Removing the legacy intro tactic code. | Pierre-Marie Pédrot | |
| 2014-11-05 | lib/RichPp: Rename into Richpp. | Yann Régis-Gianas | |
| printing/RichPrinter: Rename into Richprinter. printing/{ppvernac, ppconstr, pptactic}: Rename RichPp into Richpp. printing/Richprinter: Cosmetics. | |||
| 2014-11-05 | printing/Ppvernac: Fix missing keyword tagging on theorem introducers. | Yann Régis-Gianas | |
| 2014-11-05 | printing/Ppvernac: Fix missing keyword tagging on definition introducers. | Yann Régis-Gianas | |
| 2014-11-05 | printing/Ppvernac: Cosmetics. | Yann Régis-Gianas | |
| 2014-11-04 | printing/Ppannotation: New annotation for tactic syntactic objects. | Regis-Gianas | |
| printing/Pptactic: Tag tactics pretty-printing. printing/Ppvernac: Use the relevent Pptactic pretty-printer. printing/RichPrinter: Publish two new services. | |||
| 2014-11-04 | printing/Pptactic.Make: New. | Regis-Gianas | |
| - Functorize with respect to the pretty-printer for constr. - Include the application of Make to Ppconstr at toplevel in order to preserve previous behavior. | |||
| 2014-11-04 | printing/Pptacticsig: New signature for tactic pretty-printers. | Regis-Gianas | |
| printing/Pptactic: Use it. | |||
| 2014-11-04 | lib/Ppconstr: Cosmetics. | Regis-Gianas | |
| 2014-11-04 | Rebase artefact. | Regis-Gianas | |
| 2014-11-04 | lib/Pp.tag: New. | Regis-Gianas | |
| A combinator to introduce tags. printing/{Ppconstr, Ppvernac}: Use it. | |||
| 2014-11-04 | printing/Ppannotation: Introduce a new annotation for keywords. | Regis-Gianas | |
| printing/{Ppconstr, Ppvernac}: Use it. | |||
| 2014-11-04 | printing/richPrinter: Fix incorrect signatures. | Regis-Gianas | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |