| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-10-29 | Removing unused and useless exported function in Hints. | Pierre-Marie Pédrot | |
| 2015-10-29 | Removing the evar_map argument from s_enter. | Pierre-Marie Pédrot | |
| 2015-10-29 | Removing some goal unsafeness in inductive schemes. | Pierre-Marie Pédrot | |
| 2015-10-29 | Avoid an anomaly when destructing an unknown ident. (Fix bug #4395) | Guillaume Melquiond | |
| It is too bad that OCaml does not warn when catching an exception over a closure rather than inside it. | |||
| 2015-10-29 | Fixing another instance of bug #3267 in eauto, this time in the | Hugo Herbelin | |
| presence of hints modifying the context and of a "using" clause. Incidentally opening Hints by default in debugger. | |||
| 2015-10-29 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-28 | Univs: local names handling. | Matthieu Sozeau | |
| Keep user-side information on the names used in instances of universe polymorphic references and use them for printing. | |||
| 2015-10-28 | Avoid type checking private_constants (side_eff) again during Qed (#4357). | Enrico Tassi | |
| Side effects are now an opaque data type, called private_constant, you can only obtain from safe_typing. When add_constant is called on a definition_entry that contains private constants, they are either - inlined in the main proof term but not re-checked - declared globally without re-checking them As a safety measure, the opaque data type contains a pointer to the revstruct (an internal field of safe_env that changes every time a new constant is added), and such pointer is compared with the current value store in safe_env when the private_constant is inlined. Only when the comparison is successful the private_constant is not re-checked. Otherwise else it is. In short, we accept into the kernel private constant only when they arrive in the very same order and on top of the very same env they arrived when we fist checked them. Note: private_constants produced by workers never pass the safety measure (the revstruct pointer is an Ephemeron). Sending back the entire revstruct is possible but: 1. we lack a way to quickly compare two revstructs, 2. it can be large. | |||
| 2015-10-26 | Preserving goal name in revert/bring_hyps. | Hugo Herbelin | |
| 2015-10-26 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 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-24 | Backtracking on interpreting toplevel calls to exact in scope determined | Hugo Herbelin | |
| by the type to prove (was introduced in 35846ec22, r15978, Nov 2012). Not only it does not work when exact is called via a Ltac definition, but, also, it does not scale easily to refine which is a TACTIC EXTEND. Ideally, one may then want to propagate scope interpretations through ltac variables, as well as supporting refine... See #4034 for a discussion. | |||
| 2015-10-20 | Proofview.Goal.sigma returns an indexed evarmap. | Pierre-Marie Pédrot | |
| 2015-10-20 | Indexing Proofview.goals with a stage. | Pierre-Marie Pédrot | |
| This is not perfect though, some primitives are unsound, and some higher-order API should use polymorphic functions so as not to depend on a given level. | |||
| 2015-10-20 | Boxing the Goal.enter primitive into a record type. | Pierre-Marie Pédrot | |
| 2015-10-20 | Renaming Goal.enter field into s_enter. | Pierre-Marie Pédrot | |
| 2015-10-19 | Expliciting the uses of the old Tacmach API in Tactics. | Pierre-Marie Pédrot | |
| 2015-10-19 | Removing some unsafe uses of monotonicity. | Pierre-Marie Pédrot | |
| 2015-10-19 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-19 | Type delayed_open_constr is now monotonic. | Pierre-Marie Pédrot | |
| 2015-10-19 | Categorizing debug messages as such + NonLogical uses loggers. | Pierre Courtieu | |
| 2015-10-19 | More monotonicity in Tactics. | Pierre-Marie Pédrot | |
| 2015-10-19 | Turning anomaly into error for #4372 (weakness of inversion in the | Hugo Herbelin | |
| presence of dependent types with only superficial dependency). See discussion at https://coq.inria.fr/bugs/show_bug.cgi?id=4372. | |||
| 2015-10-19 | Removing tclEVARS in various places. | Pierre-Marie Pédrot | |
| 2015-10-19 | Reducing the uses of tclEVARS in Tactics by using monotonous functions. | Pierre-Marie Pédrot | |
| 2015-10-18 | Making Evarutil.new_evar monotonous. | Pierre-Marie Pédrot | |
| 2015-10-18 | Constraining refine to monotonic functions. | Pierre-Marie Pédrot | |
| 2015-10-17 | Clarifying and documenting the UState API. | Pierre-Marie Pédrot | |
| 2015-10-16 | Generalize fix for auto from PMP to eauto and typeclasses eauto. | Matthieu Sozeau | |
| 2015-10-16 | Merge branch 'v8.5' into trunk | Maxime Dénès | |
| 2015-10-16 | Merge hint lists instead of appending them. (Fix bug #3199) | Guillaume Melquiond | |
| 2015-10-15 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-14 | Fixing perfomance issue of auto hints induced by universes. | Pierre-Marie Pédrot | |
| Instead of brutally merging the whole evarmap coming from the clenv, we remember the context associated to the hint and we only merge that tiny part of constraints. We need to be careful for polymorphic hints though, as we have to refresh them beforehand. | |||
| 2015-10-14 | Exporting the original unprocessed hint in the hint running function. | Pierre-Marie Pédrot | |
| 2015-10-13 | Fix some typos. | Guillaume Melquiond | |
| 2015-10-12 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-12 | Remove code that was already commented out. | Maxime Dénès | |
| 2015-10-11 | Fixing bug #4366: Conversion tactics recheck uselessly convertibility. | Pierre-Marie Pédrot | |
| 2015-10-11 | Fixing untimely unexpected warning "Collision between bound variables" (#4317). | Hugo Herbelin | |
| Collecting the bound variables is now done on the glob_constr, before interpretation, so that only variables given explicitly by the user are used for binding bound variables. | |||
| 2015-10-10 | Merge branch 'v8.5' | 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 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-06 | Fix bug #4354: interpret hints in the right env and sigma. | Matthieu Sozeau | |
| 2015-10-02 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-02 | Univs: refined handling of assumptions | Matthieu Sozeau | |
| According to their polymorphic/non-polymorphic status, which imply that universe variables introduced with it are assumed to be >= or > Set respectively in the following definitions. | |||
| 2015-10-02 | Univs: fix evar_map handling in Hint processing. | Matthieu Sozeau | |
| 2015-10-02 | discriminate: Do fresh_global in the right env in presence of side-effects. | Matthieu Sozeau | |
| 2015-10-02 | Univs: fix many evar_map initializations and leaks. | Matthieu Sozeau | |
| 2015-09-27 | Removing uselessly duplicated function in Evd. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |