| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-12-25 | Fixing an "injection as" bug in the presence of side conditions. | Hugo Herbelin | |
| 2015-12-25 | Moving the ad hoc interpretation of "intros" as "intros **" from tacinterp.ml | Hugo Herbelin | |
| to g_tactic.ml4 so as to leave room for "IntroPattern []" to mean "no introduction". | |||
| 2015-12-24 | Removing auto from the tactic AST. | Pierre-Marie Pédrot | |
| 2015-12-24 | Removing the last quoted auto tactic in Tauto. | Pierre-Marie Pédrot | |
| 2015-12-21 | Finer-grained types for toplevel values. | Pierre-Marie Pédrot | |
| 2015-12-21 | Removing ad-hoc interpretation rules for tactic notations and their genarg. | Pierre-Marie Pédrot | |
| Now that types can share the same dynamic representation, we do not have to transtype the topelvel values dynamically and just take advantage of the standard interpretation function. | |||
| 2015-12-21 | Changing the toplevel type of the int_or_var generic type to int. | Pierre-Marie Pédrot | |
| 2015-12-21 | Removing the now useless genarg generic argument. | Pierre-Marie Pédrot | |
| 2015-12-21 | Using dynamic values in tactic evaluation. | Pierre-Marie Pédrot | |
| 2015-12-18 | Tying the loop in tactic printing API. | Pierre-Marie Pédrot | |
| 2015-12-17 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-12-17 | Getting rid of some hardwired generic arguments. | Pierre-Marie Pédrot | |
| 2015-12-16 | FIx parsing of tactic "simple refine". | Maxime Dénès | |
| 2015-12-16 | Add a "simple refine" variant of "refine" that does not call "shelve_unifiable". | Guillaume Melquiond | |
| 2015-12-15 | Refine tactic now shelves unifiable holes. | Pierre-Marie Pédrot | |
| The unshelve tactical can be used to get the shelved holes. This changes the proper ordering of holes though, so expect some broken scripts. Also, the test-suite is not fixed yet. | |||
| 2015-12-15 | Changing the order of the goals generated by unshelve. | Pierre-Marie Pédrot | |
| 2015-12-15 | Granting clear_flag in injection, even legacy mode. This is possible | Hugo Herbelin | |
| since the clear_flag is new. | |||
| 2015-12-13 | More code sharing between tactic notation and genarg interpretation. | Pierre-Marie Pédrot | |
| 2015-12-11 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-12-11 | Add tactic native_cast_no_check, analog to vm_cast_no_check. | Maxime Dénès | |
| 2015-12-10 | Fixing a pat%constr bug. Thanks to Enrico for reporting. | Hugo Herbelin | |
| 2015-12-10 | Silently ignore requests to _not_ clear something when that something cannot ↵ | Guillaume Melquiond | |
| be cleared. This should fix the contrib failures on tactics like "destruct (0)". | |||
| 2015-12-09 | Fixing parsing of the unshelve tactical. | Pierre-Marie Pédrot | |
| Now [unshelve tac1; tac2] is parsed as [(unshelve tac1); tac2]. | |||
| 2015-12-09 | Adding an unshelve tactical. | Pierre-Marie Pédrot | |
| This tactical is inspired by discussions on the Coq-club list. For now it is still undocumented, and there is room left for design issues. | |||
| 2015-12-08 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-12-07 | Fix some typos. | Guillaume Melquiond | |
| 2015-12-05 | Fixing compilation with old CAMLPX versions. | Pierre-Marie Pédrot | |
| 2015-12-05 | Removing redundant versions of generalize. | Hugo Herbelin | |
| 2015-12-05 | Moving extended_rel_vect/extended_rel_list to the kernel. | Hugo Herbelin | |
| It will later be used to fix a bug and improve some code. Interestingly, there were a redundant semantic equivalent to extended_rel_list in the kernel called local_rels, and another private copy of extended_rel_list in exactly the same file. | |||
| 2015-12-05 | Experimenting removing strong normalization of the mid-statement in tactic cut. | Hugo Herbelin | |
| 2015-12-05 | Moving three related small half-general half-ad-hoc utility functions | Hugo Herbelin | |
| next to each other, waiting for possible integration into a more uniform API. | |||
| 2015-12-05 | Getting rid of some quoted tactics in Tauto. | Pierre-Marie Pédrot | |
| 2015-12-04 | Getting rid of the dynamic node of the tactic AST. | Pierre-Marie Pédrot | |
| 2015-12-04 | Fix in setoid_rewrite in Type: avoid the generation of a rigid universe | Matthieu Sozeau | |
| on applications of inverse (flip) on a crelation. This was poluting universe constraints of lemmas using generalized rewriting in Type. | |||
| 2015-12-04 | Removing the last use of valueIn in Tauto. | Pierre-Marie Pédrot | |
| 2015-12-04 | Removing dynamic inclusion of constrs in tactic AST. | Pierre-Marie Pédrot | |
| 2015-12-03 | Removing the globTacticIn primitive. | Pierre-Marie Pédrot | |
| It was not used in Coq codebase, and the only known user was ssreflect up to commit 95354e0dee. | |||
| 2015-12-03 | Fixing Tauto compilation for older versions of OCaml. | Pierre-Marie Pédrot | |
| 2015-12-03 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-12-03 | Removing the last use of tacticIn in setoid_ring. | Pierre-Marie Pédrot | |
| 2015-12-03 | Removing the use of tacticIn in Tauto. | Pierre-Marie Pédrot | |
| 2015-12-02 | Slight simplification of code for pat/constr. | Hugo Herbelin | |
| 2015-12-02 | Dead code from August 2014 in apply in. | Hugo Herbelin | |
| 2015-12-02 | Removing dead code in Obligations. | Pierre-Marie Pédrot | |
| 2015-11-29 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-11-27 | Fix [Polymorphic Hint Rewrite]. | Matthieu Sozeau | |
| 2015-11-26 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-11-23 | Fix generation of equality schemes on polymorphic equality types. | Matthieu Sozeau | |
| 2015-11-23 | Removing a use of old refine in Tactics. | Pierre-Marie Pédrot | |
| 2015-11-20 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |