| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-12-25 | Fixing non exhaustive pattern-matching in 003fe3d5e60b. | Hugo Herbelin | |
| 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-23 | Partial backtrack on commit 20641795624. | Pierre-Marie Pédrot | |
| The parsing rules were broken and disallowed tactic replacement of the form Ltac ident ::= expr. | |||
| 2015-12-22 | Avoid a pointless conversion/copy. | Guillaume Melquiond | |
| 2015-12-22 | Do not compose "str" and "to_string" whenever possible. | Guillaume Melquiond | |
| For instance, calling only Id.print is faster than calling both str and Id.to_string, since the latter performs a copy. It also makes the code a bit simpler to read. | |||
| 2015-12-22 | COMMENTS: of "Constr.case_info" type were updated. | Matej Kosik | |
| 2015-12-22 | COMMENTS: added to the "Names.inductive" and "Names.constructor" types. | Matej Kosik | |
| 2015-12-22 | Inclusion of functors with restricted signature is now forbidden (fix #3746) | Pierre Letouzey | |
| The previous behavior was to include the interface of such a functor, possibly leading to the creation of unexpected axioms, see bug report #3746. In the case of non-functor module with restricted signature, we could simply refer to the original objects (strengthening), but for a functor, the inner objects have no existence yet. As said in the new error message, a simple workaround is hence to first instantiate the functor, then include the local instance: Module LocalInstance := Funct(Args). Include LocalInstance. By the way, the mod_type_alg field is now filled more systematically, cf new comments in declarations.mli. This way, we could use it to know whether a module had been given a restricted signature (via ":"). Earlier, some mod_type_alg were None in situations not handled by the extraction (MEapply of module type). Some code refactoring on the fly. | |||
| 2015-12-22 | Move the From logic to Loadpath.expand_path. | Guillaume Melquiond | |
| 2015-12-22 | Do not query module files that have already been loaded. | Guillaume Melquiond | |
| For a script that does just "Require Reals", this avoids 40k queries. Note that this changes the signature of the FileDependency feedback. Indeed, it no longer provides the physical path to the dependency but only its logical path (since the physical path is no longer available). The physical path could still have been recovered thanks to the libraries_filename_table list. But due to the existence of the overwrite_library_filenames function, its content cannot be trusted. So anyone interested in the actual physical path should now also rely on the FileLoaded feedback. | |||
| 2015-12-21 | ARGUMENT EXTEND shares the toplevel representation when possible. | 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 | Sharing toplevel representation for several generic types. | Pierre-Marie Pédrot | |
| - int and int_or_var - ident and var - constr and constr_may_eval | |||
| 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-21 | Attaching a dynamic argument to the toplevel type of generic arguments. | Pierre-Marie Pédrot | |
| 2015-12-21 | Trust the directory cache in batch mode. | Guillaume Melquiond | |
| When coqtop is a long-lived process (e.g. coqide), the user might be creating files on the fly. So we have to ask the operating system whether a file exists beforehand, so that we know whether the content of the directory cache is outdated. In batch mode, we can assume that the cache is always up-to-date, so we don't need to query the operating system before trusting the content of the cache. On a script doing "Require Import Reals", this brings down the number of stat syscalls from 42k to 2k. The number of syscalls could be further halved if all_subdirs was filling the directory cache. | |||
| 2015-12-18 | COMMENTS: added to the "Constr.case_info" type. | Matej Kosik | |
| 2015-12-18 | CLEANUP: the definition of the "Constrexpr.case_expr" type was simplified | Matej Kosik | |
| 2015-12-18 | CLEANUP: removing unnecessary alias | Matej Kosik | |
| 2015-12-18 | CLEANUP: Vernacexpr.VernacDeclareTacticDefinition | Matej Kosik | |
| The definition of Vernacexpr.VernacDeclareTacticDefinition was changed. The original definition allowed us to represent non-sensical value such as: VernacDeclareTacticDefinition(Qualid ..., false, ...) The new definition prevents that. | |||
| 2015-12-18 | TYPOGRAPHY: correction of one particular error in the Reference Manual | Matej Kosik | |
| 2015-12-18 | CLEANUP: Removing "Vernacexpr.VernacNop" variant to which no Vernacular ↵ | Matej Kosik | |
| command is mapped. | |||
| 2015-12-18 | CLEANUP: simplifying "Coqtop.init_gc" implementation | Matej Kosik | |
| 2015-12-18 | CLEANUP: removing unnecessary wrapper function | Matej Kosik | |
| 2015-12-18 | COMMENTS: added to some variants of "Globalnames.global_reference" type. | Matej Kosik | |
| 2015-12-18 | COMMENTS: added to some variants of "Misctypes.glob_sort_gen" type. | Matej Kosik | |
| 2015-12-18 | COMMENTS: added to some variants of "Glob_term.glob_constr" type. | Matej Kosik | |
| 2015-12-18 | COMMENTS: added to some variants of the "Constrexpr.prim_token" type. | Matej Kosik | |
| 2015-12-18 | ALPHA-CONVERSION: in "parsing/g_vernac.ml4" file | Matej Kosik | |
| 2015-12-18 | COMMENTS: added to the "Unicode" module. | Matej Kosik | |
| 2015-12-18 | COMMENTS: updated in the "Option" module. | Matej Kosik | |
| 2015-12-18 | COMMENTS: added to some variants of the "Constr.kind_of_term" type. | Matej Kosik | |
| 2015-12-18 | CLEANUP: Vernacexpr.vernac_expr | Matej Kosik | |
| Originally, "VernacTime" and "VernacRedirect" were defined like this: type vernac_expr = ... | VernacTime of vernac_list | VernacRedirect of string * vernac_list ... where type vernac_list = located_vernac_expr list Currently, that list always contained one and only one element. So I propose changing the definition of these two variants in the following way: | VernacTime of located_vernac_expr | VernacRedirect of string * located_vernac_expr which covers all our current needs and enforces the invariant related to the number of commands that are part of the "VernacTime" and "VernacRedirect" variants. | |||
| 2015-12-18 | COMMENTS: added to the "Predicate" module | Matej Kosik | |
| In the original version, ocamldoc markup wasn't used properly thus ocamldoc output did not in all places make sense. This commit makes sure that the documentation of the Predicate module is as clear as the documentation of the Set module (in the standard library). | |||
| 2015-12-18 | COMMENTS: added to the "Names" module. | Matej Kosik | |
| 2015-12-18 | Tying the loop in tactic printing API. | Pierre-Marie Pédrot | |
| 2015-12-17 | (Partial) fix for bug #4453: raise an error instead of an anomaly. | Matthieu Sozeau | |
| 2015-12-17 | spawn: fix leak of file descriptors | Enrico Tassi | |
| The interesting manifestation of the bug was Unix.select returning no error but the empty list of descriptors, as if a timeout did happen. | |||
| 2015-12-17 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-12-17 | ALPHA-CONVERSION: in the "Reduction" module: clos_fconv --> clos_gen_conv | Matej Kosik | |
| 2015-12-17 | ALPHA-CONVERSION: in the "Reduction" module: fconv --> gen_conv | Matej Kosik | |
| 2015-12-17 | CLEANUP: in the Reduction module | Matej Kosik | |
| 2015-12-17 | CLEANUP: in the Reductionops module | Matej Kosik | |
| 2015-12-17 | CLEANUP: in the Reduction module | Matej Kosik | |
| 2015-12-17 | Getting rid of some hardwired generic arguments. | Pierre-Marie Pédrot | |
| 2015-12-16 | Updating credits. | Hugo Herbelin | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |