| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 2015-11-19 | Fix bug #4429: eauto with arith: 70x performance regression in Coq 8.5. | Pierre-Marie Pédrot | |
| The issue was due to the fact that unfold hints are given a priority of 4 by default. As eauto was now using hint priority rather than the number of goals produced to order the application of hints, unfold were almost always used too late. We fixed this by manually giving them a priority of 1 in the eauto tactic. Also fixed the relative order of proof depth w.r.t. hint priority. It should not be observable except for breadth-first search, which is seldom used. | |||
| 2015-11-19 | Fix bug #4433, removing hack on evars appearing in a pattern from a | Matthieu Sozeau | |
| constr, and the associated signature, not needed anymore. Update CHANGES, no evar_map is produced by pattern_of_constr anymore. | |||
| 2015-11-18 | Improve error message. | Maxime Dénès | |
| 2015-11-18 | Inlining the only use of Clenv.connect_clenv. | Pierre-Marie Pédrot | |
| 2015-11-17 | More optimizations of [Clenv.clenv_fchain]. | Pierre-Marie Pédrot | |
| Everywhere we know that the universes of the left argument are an extension of the right argument, we do not have to merge universes. | |||
| 2015-11-17 | Performance fix for destruct. | Pierre-Marie Pédrot | |
| The clenv_fchain function was needlessly merging universes coming from two evarmaps even though one was an extension of the other. A flag was added so that the tactic just retrieves the newer universes. | |||
| 2015-11-15 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-11-13 | Continue fix of PMP, handling setoid_rewrite in let-bound hyps correctly. | Matthieu Sozeau | |
| 2015-11-11 | Fix bug #3257, setoid_reflexivity should fail if not completing the goal. | Matthieu Sozeau | |
| 2015-11-10 | Activating bracketing of last or-and introduction pattern by default | Hugo Herbelin | |
| for more regularity. | |||
| 2015-11-10 | Merge origin/v8.5 into trunk | Hugo Herbelin | |
| Did some manual merge in tactics/tactics.ml. | |||
| 2015-11-10 | Typo. | Hugo Herbelin | |
| 2015-11-10 | Fix bug #4404: [remember] gives Error: Conversion test raised an anomaly. | Pierre-Marie Pédrot | |
| 2015-11-07 | Implementing assert and cut with LetIn rather than using a beta-redex. | Hugo Herbelin | |
| Hopefully, it will provide with nicer proof terms, in combination with the commit printing the type of LetIn when the defined term is a proof. | |||
| 2015-11-07 | Preservation of the name of evars/goals when applying pose/set/intro/clearbody. | Hugo Herbelin | |
| For pose/set/clearbody, I think it is clear that we want to preserve the name and this commit do it. For revert, I first did not preserve the name, then considered in 2ba2ca96be88 that it was better to preserve it. For intro, like for revert actually, I did not preserve the name, based on the idea that the type was changing (*). For instance if we have ?f:nat->nat, do we really want to keep the name f in ?f:nat after an intro. For revert, I changed my mind based on the idea that if we had a better control of the name if we keep the name that if the system invents a new one based on the type. I think this is more reasonable than (*), so this commit preserves the name for intro. For generalize, it is still not done because of generalize being in the old proof engine. | |||
| 2015-11-07 | Merge remote-tracking branch 'origin/v8.5' into upstream-trunk | Hugo Herbelin | |
| - Had to add a Sigma.to_evar_map - Had to rework coqdep_common.ml{,i} and coqdep.ml | |||
| 2015-11-05 | Fix bug #4273 | Matthieu Sozeau | |
| Syntactic analysis of dependencies when atomizing arguments in destruct was not dealing properly with primitive projections hiding their parameters. | |||
| 2015-11-05 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-11-04 | Hint Cut documentation and cleanup of printing (was duplicated and | Matthieu Sozeau | |
| inconsistent). | |||
| 2015-11-04 | Fix bug in proofs/logic.ml type_of_global_reference_knowing_conclusion | Matthieu Sozeau | |
| is buggy in general. | |||
| 2015-11-02 | Fix bug #4397: refreshing types in abstract_generalize. | Matthieu Sozeau | |
| 2015-11-02 | Fix bug #4151: discrepancy between exact and eexact/eassumption. | Matthieu Sozeau | |
| 2015-10-30 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-29 | Monotonizing Tactics.change_arg. | Pierre-Marie Pédrot | |
| 2015-10-29 | Removing some goal unsafeness in Equality. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |