| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-01-21 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-01-20 | Update copyright headers. | Maxime Dénès | |
| 2016-01-02 | Remove some unused functions. | Guillaume Melquiond | |
| Note: they do not even seem to have a debugging purpose, so better remove them before they bitrot. | |||
| 2015-12-28 | Eradicating uses of open_constr in TACTIC EXTEND in favour of uconstr. | Pierre-Marie Pédrot | |
| 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-04 | Hint Cut documentation and cleanup of printing (was duplicated and | Matthieu Sozeau | |
| inconsistent). | |||
| 2015-10-24 | Fixing a loop in checking hints with holes. | Hugo Herbelin | |
| For instance, "Hint Resolve (fst _ _)." was looping (bug in 841bc461). | |||
| 2015-10-16 | Merge hint lists instead of appending them. (Fix bug #3199) | Guillaume Melquiond | |
| 2015-10-14 | Exporting the original unprocessed hint in the hint running function. | Pierre-Marie Pédrot | |
| 2015-10-09 | Refine fix for handling of the universe contexts of hints, depending on | Matthieu Sozeau | |
| their polymorphic status _and_ locality. | |||
| 2015-10-09 | Fix CFGV contrib: handling of global hints introducing global universes. | Matthieu Sozeau | |
| It was wrong, the context was readded needlessly to the local evar_map context. | |||
| 2015-10-06 | Fix bug #4354: interpret hints in the right env and sigma. | Matthieu Sozeau | |
| 2015-10-02 | Univs: fix evar_map handling in Hint processing. | Matthieu Sozeau | |
| 2015-10-02 | Univs: fix many evar_map initializations and leaks. | Matthieu Sozeau | |
| 2015-05-13 | Safer typing primitives. | Pierre-Marie Pédrot | |
| Some functions from pretyping/typing.ml and their derivatives were potential source of evarmap leaks, as they dropped their resulting evarmap. This commit clarifies the situation by renaming them according to a unsafe_* scheme. Their sound variant is likewise renamed to their old name. The following renamings were made. - Typing.type_of -> unsafe_type_of - Typing.e_type_of -> type_of - A new e_type_of function that matches the e_ prefix policy - Tacmach.pf_type_of -> pf_unsafe_type_of - A new safe pf_type_of function. All uses of unsafe_* functions should be eventually eliminated. | |||
| 2015-05-12 | Adding an option Loose Hint Behavior to handle hints loaded but not imported. | Pierre-Marie Pédrot | |
| It accepts three distinct flags: - "Lax", which is the default one, sets the old behaviour, i.e. a non-imported hint behaves the same as an imported one. - "Warn" outputs a warning when a non-imported hint is used. Note that this is an over-approximation, because a hint may be triggered by an eauto run that will eventually fail and backtrack. - "Strict" changes the behaviour of an unloaded hint to the one of the fail tactic, allowing to emulate the hopefully future import-scoped hint mechanism. | |||
| 2015-05-12 | Adding unique identifiers to hints. | Pierre-Marie Pédrot | |
| 2015-05-11 | Rationalizing a bit the interface of Hints. | Pierre-Marie Pédrot | |
| 2015-04-23 | Remove almost all the uses of string concatenation when building error messages. | Guillaume Melquiond | |
| Since error messages are ultimately passed to Format, which has its own buffers for concatenating strings, using concatenation for preparing error messages just doubles the workload and increases memory pressure. | |||
| 2015-04-16 | Ensuring purity of datastructures in the API. | Pierre-Marie Pédrot | |
| 2015-04-14 | Cleaning up the implementation of search entries in Hints. | Pierre-Marie Pédrot | |
| 2015-04-14 | Opaque implementation of auto tactics. | Pierre-Marie Pédrot | |
| We provide an eliminator ensuring that the AST will be used to build a tactic, so that we can stuff arbitrary things inside. An escape function is also provided for backward compatibility. | |||
| 2015-04-13 | More documented representation of hint objects. | Pierre-Marie Pédrot | |
| 2015-03-03 | Fix bug #3590, keeping evars that are not turned into named metas by | Matthieu Sozeau | |
| pattern_of_constr in an evar_map, as they can appear in the context of said named metas, which is used by change. Not sure what to do in the PEvar case, which never matches anyway according to Constr_matching.matches. | |||
| 2015-01-12 | Update headers. | Maxime Dénès | |
| 2014-10-27 | Removing the last Evd.diff from Hints. | Pierre-Marie Pédrot | |
| 2014-10-08 | Forgotten hints.ml{,i} files in 38b34dfffcc. | Hugo Herbelin | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |