| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 2015-09-25 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-09-23 | Hopefully better names to constructors of internal_flag, as discussed | Hugo Herbelin | |
| with Enrico. | |||
| 2015-09-23 | Give a way to control if the decidable-equality schemes are built like | Hugo Herbelin | |
| in 8.4 with the schemes of the subcomponent of an inductive added to the environment or discharged as let-ins over the main scheme. As of today, decidable-equality schemes are built when calling vernacular command (Inductive with option Set Dedicable Equality Schemes, or Scheme Equality), so there is no need to discharge the sub-schemes as let-ins. But if ever the schemes are built from within an opaque proof and one would not like the schemes and a fortiori the subschemes to appear in the env, the new addition of a parameter internal_flag to "find_scheme" allows this possibility (then to be set to KernelSilent). | |||
| 2015-09-22 | Fixing bug #4207: setoid_rewrite creates self-referring hypotheses. | Pierre-Marie Pédrot | |
| We purge the environment given to the morphism searcher from all dependencies on the considered variable. I hope it is not too costly. | |||
| 2015-09-17 | Merge branch 'v8.5' into trunk | Maxime Dénès | |
| 2015-09-16 | In pat/constr introduction patterns, fixing in a better way clearing problems | Hugo Herbelin | |
| of temporary hypotheses than 76f27140e6e34 did. | |||
| 2015-09-16 | Continuing investigation on how to preserve the locality of the action | Hugo Herbelin | |
| of "apply ... in ... as ..." in the context. Fixing a regression done by 7e00e8d60 and f2130a88e1: when an evar is created, the statement of the refined hypothesis virtually depends on the whole context and has to be left at the top. | |||
| 2015-09-14 | Univs: Add universe binding lists to definitions | Matthieu Sozeau | |
| ... lemmas and inductives to control which universes are bound and where in universe polymorphic definitions. Names stay outside the kernel. | |||
| 2015-09-10 | fresh now accepts more things than just identifiers. | Pierre Courtieu | |
| Namely, it accepts, variables, constants, inductives and constructors. When these have a qualified name, the fresh is done on its basename. | |||
| 2015-09-09 | Merge remote-tracking branch 'origin/v8.5' into trunk | Hugo Herbelin | |
| 2015-09-08 | Fixing incomplete bugfix in 76f27140e6e34 (unfortunately 5 commits | Hugo Herbelin | |
| ago) which broke compilation of theories/Logic/WKL.v (collision between a temporary name and a user name). | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |