| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-04-27 | Attempt to slightly improve abusive "Collision between bound | Hugo Herbelin | |
| variables" when matching over "{v : _ | _ & _}" which hides twice the binding "fun v" since it is "sig2 (fun v => _) (fun v => _)". Computing the bound variables statically at internalisation time rather than every time at interpretation time. This cannot hurt even if I don't know how to deal with the "notation" problem of a single bound variable actually hiding two: at the current time, the notation is printed only if the two variables are identical (see #4592), so, with this semantics the warning should not be printed, but we lost the information that we are coming from a notation; if #4592 were addressed, then one of the binding should be alpha-renamed if they differ, so collision should be solved by choosing the variable name which is not renamed, but the matching algorithm should then be aware of what the notation printing algorithm is doing... maybe not the most critical thing at the current time. | |||
| 2016-04-25 | Merging the ML tactic notation and plain Tactic Notation mechanisms. | Pierre-Marie Pédrot | |
| 2016-04-25 | Factorizing code in tactic notations. | Pierre-Marie Pédrot | |
| 2016-04-25 | Documenting API. | Pierre-Marie Pédrot | |
| 2016-04-24 | Remove dead registering code in Pcoq. | Pierre-Marie Pédrot | |
| 2016-04-24 | Disentangle tactic notation resolution from Pcoq. | Pierre-Marie Pédrot | |
| Instead of relying on entry names as given by a hardwired registering scheme in Pcoq, we recover them first through a user-defined map, and fallback on generic argument names. | |||
| 2016-04-24 | Higher-level API for tactic notations. | Pierre-Marie Pédrot | |
| 2016-04-24 | Factorizing the declaration of ML notation printing in Tacentries. | Pierre-Marie Pédrot | |
| 2016-04-14 | Moving and enhancing the grammar_tactic_prod_item_expr type. | Pierre-Marie Pédrot | |
| 2016-04-12 | Adding toplevel representation sharing for some generic arguments. | Pierre-Marie Pédrot | |
| 2016-04-12 | Removing redundant *_TYPED AS clauses in EXTEND statements. | Pierre-Marie Pédrot | |
| 2016-04-11 | Removing the ad-hoc tactic_expr type. | Pierre-Marie Pédrot | |
| This type was actually only used by the debug printer of tactics, and only for atomic tactics. Furthermore, that type was asymmetric, as the underlying tacexpr type was set to be glob_tactic, when the semantics would have required a Val.t type. Furthermore, this type is absent from every contrib I have seen, which hints again in favour of its lack of meaning. | |||
| 2016-04-09 | Removing extra spaces in printing arguments of VERNAC EXTEND. | Hugo Herbelin | |
| 2016-04-09 | Re-add printer for tacdef_body so that Ltac definitions are printed by ↵ | Hugo Herbelin | |
| pr_vernac. | |||
| 2016-04-09 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-04-08 | Fixing printing of toplevel values. | Pierre-Marie Pédrot | |
| This is not perfect yet, in particular the whole precedence system is a real mess, as there is a real need for tidying up the Pptactic implementation. Nonetheless, printing toplevel values is only used for debugging purposes, where an ugly display is better than none at all. | |||
| 2016-04-01 | Getting rid of the "_mods" parsing entry. | Pierre-Marie Pédrot | |
| It was only used by setoid_ring for the Add Ring command, and was easily replaced by a dedicated argument. Moreover, it was of no use to tactic notations. | |||
| 2016-03-31 | Moving the code handling tactic notations to Tacentries. | Pierre-Marie Pédrot | |
| 2016-03-31 | Moving the Tactic Notation entry parser from Pcoq to Tacentries. | Pierre-Marie Pédrot | |
| 2016-03-28 | Fixing an incorrect use of prod_appvect on a term which was not a | Hugo Herbelin | |
| product in setoid_rewrite. Before commit e8c47b652, it was raising an error which has been turned to an anomaly. This impacted Compcert where the former error was (apparently) caught so that setoid_rewrite was returning back to ordinary rewrite. | |||
| 2016-03-28 | Fixing an evar leak in Rewrite introduced by 968dfdb15. | Pierre-Marie Pédrot | |
| 2016-03-25 | Moving Autorewrite back to tactics/. | Pierre-Marie Pédrot | |
| 2016-03-25 | Making Autorewrite independent from Ltac. | Pierre-Marie Pédrot | |
| 2016-03-25 | Moving Eqdecide to tactics/. | Pierre-Marie Pédrot | |
| 2016-03-25 | Making Eqdecide independent of Extratactics. | Pierre-Marie Pédrot | |
| 2016-03-25 | Moving Eauto and Class_tactics to tactics/. | Pierre-Marie Pédrot | |
| 2016-03-25 | Moving type_uconstr to Pretyping. | Pierre-Marie Pédrot | |
| 2016-03-21 | Creating a dedicated ltac/ folder for Hightactics. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |