| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-12-25 | Fixing an "injection as" bug in the presence of side conditions. | Hugo Herbelin | |
| 2015-12-25 | Moving the ad hoc interpretation of "intros" as "intros **" from tacinterp.ml | Hugo Herbelin | |
| to g_tactic.ml4 so as to leave room for "IntroPattern []" to mean "no introduction". | |||
| 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 | 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 | 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 | |
| 2015-12-16 | Update version numbers and magic numbers for 8.5rc1 release. | Maxime Dénès | |
| 2015-12-16 | FIx parsing of tactic "simple refine". | Maxime Dénès | |
| 2015-12-16 | Add a "simple refine" variant of "refine" that does not call "shelve_unifiable". | Guillaume Melquiond | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |