aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Removing auto from the tactic AST.Gravatar Pierre-Marie Pédrot2015-12-24
|
* Removing the last quoted auto tactic in Tauto.Gravatar Pierre-Marie Pédrot2015-12-24
|
* Partial backtrack on commit 20641795624.Gravatar Pierre-Marie Pédrot2015-12-23
| | | | | | The parsing rules were broken and disallowed tactic replacement of the form Ltac ident ::= expr.
* Avoid a pointless conversion/copy.Gravatar Guillaume Melquiond2015-12-22
|
* Do not compose "str" and "to_string" whenever possible.Gravatar Guillaume Melquiond2015-12-22
| | | | | | 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.
* Move the From logic to Loadpath.expand_path.Gravatar Guillaume Melquiond2015-12-22
|
* Do not query module files that have already been loaded.Gravatar Guillaume Melquiond2015-12-22
| | | | | | | | | | | | | 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.
* ARGUMENT EXTEND shares the toplevel representation when possible.Gravatar Pierre-Marie Pédrot2015-12-21
|
* Finer-grained types for toplevel values.Gravatar Pierre-Marie Pédrot2015-12-21
|
* Removing ad-hoc interpretation rules for tactic notations and their genarg.Gravatar Pierre-Marie Pédrot2015-12-21
| | | | | | 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.
* Sharing toplevel representation for several generic types.Gravatar Pierre-Marie Pédrot2015-12-21
| | | | | | - int and int_or_var - ident and var - constr and constr_may_eval
* Changing the toplevel type of the int_or_var generic type to int.Gravatar Pierre-Marie Pédrot2015-12-21
|
* Removing the now useless genarg generic argument.Gravatar Pierre-Marie Pédrot2015-12-21
|
* Using dynamic values in tactic evaluation.Gravatar Pierre-Marie Pédrot2015-12-21
|
* Attaching a dynamic argument to the toplevel type of generic arguments.Gravatar Pierre-Marie Pédrot2015-12-21
|
* Trust the directory cache in batch mode.Gravatar Guillaume Melquiond2015-12-21
| | | | | | | | | | | | | | | 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.
* COMMENTS: added to the "Constr.case_info" type.Gravatar Matej Kosik2015-12-18
|
* CLEANUP: the definition of the "Constrexpr.case_expr" type was simplifiedGravatar Matej Kosik2015-12-18
|
* CLEANUP: removing unnecessary aliasGravatar Matej Kosik2015-12-18
|
* CLEANUP: Vernacexpr.VernacDeclareTacticDefinitionGravatar Matej Kosik2015-12-18
| | | | | | | | | | 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.
* TYPOGRAPHY: correction of one particular error in the Reference ManualGravatar Matej Kosik2015-12-18
|
* CLEANUP: Removing "Vernacexpr.VernacNop" variant to which no Vernacular ↵Gravatar Matej Kosik2015-12-18
| | | | command is mapped.
* CLEANUP: simplifying "Coqtop.init_gc" implementationGravatar Matej Kosik2015-12-18
|
* CLEANUP: removing unnecessary wrapper functionGravatar Matej Kosik2015-12-18
|
* COMMENTS: added to some variants of "Globalnames.global_reference" type.Gravatar Matej Kosik2015-12-18
|
* COMMENTS: added to some variants of "Misctypes.glob_sort_gen" type.Gravatar Matej Kosik2015-12-18
|
* COMMENTS: added to some variants of "Glob_term.glob_constr" type.Gravatar Matej Kosik2015-12-18
|
* COMMENTS: added to some variants of the "Constrexpr.prim_token" type.Gravatar Matej Kosik2015-12-18
|
* ALPHA-CONVERSION: in "parsing/g_vernac.ml4" fileGravatar Matej Kosik2015-12-18
|
* COMMENTS: added to the "Unicode" module.Gravatar Matej Kosik2015-12-18
|
* COMMENTS: updated in the "Option" module.Gravatar Matej Kosik2015-12-18
|
* COMMENTS: added to some variants of the "Constr.kind_of_term" type.Gravatar Matej Kosik2015-12-18
|
* CLEANUP: Vernacexpr.vernac_exprGravatar Matej Kosik2015-12-18
| | | | | | | | | | | | | | | | | | | | | | | | 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.
* COMMENTS: added to the "Predicate" moduleGravatar Matej Kosik2015-12-18
| | | | | | | | 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).
* COMMENTS: added to the "Names" module.Gravatar Matej Kosik2015-12-18
|
* Tying the loop in tactic printing API.Gravatar Pierre-Marie Pédrot2015-12-18
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-17
|\
* | ALPHA-CONVERSION: in the "Reduction" module: clos_fconv --> clos_gen_convGravatar Matej Kosik2015-12-17
| |
* | ALPHA-CONVERSION: in the "Reduction" module: fconv --> gen_convGravatar Matej Kosik2015-12-17
| |
* | CLEANUP: in the Reduction moduleGravatar Matej Kosik2015-12-17
| |
* | CLEANUP: in the Reductionops moduleGravatar Matej Kosik2015-12-17
| |
* | CLEANUP: in the Reduction moduleGravatar Matej Kosik2015-12-17
| |
* | Getting rid of some hardwired generic arguments.Gravatar Pierre-Marie Pédrot2015-12-17
| |
| * Updating credits.Gravatar Hugo Herbelin2015-12-16
| |
| * Update version numbers and magic numbers for 8.5rc1 release.Gravatar Maxime Dénès2015-12-16
| |
| * FIx parsing of tactic "simple refine".Gravatar Maxime Dénès2015-12-16
| |
| * Add a "simple refine" variant of "refine" that does not call "shelve_unifiable".Gravatar Guillaume Melquiond2015-12-16
| |
| * Extraction: slightly better heuristic for Obj.magic simplificationsGravatar Pierre Letouzey2015-12-16
| | | | | | | | | | | | | | | | | | | | On an application (f args) where the head is magic, we first remove Obj.magic on arguments before continuing with simplifications (that may push magic down inside the arguments). For instance, starting with ((Obj.magic f) (Obj.magic (g h))), we now end with ((Obj.magic f) (g h)) instead of ((Obj.magic f) ((Obj.magic g) h))) as before.
| * Extraction: fixed beta-red with Obj.magic (#2795 again) + other simplificationsGravatar Pierre Letouzey2015-12-16
| | | | | | | | | | | | | | | | | | | | | | Unfortunately, my first attempt at replacing (Obj.magic (fun x -> u) v) by ((fun x -> Obj.magic u) v) was badly typed, as seen in FingerTree: the argument v should also be magic now, otherwise it might not have the same type as x. This optimization is now correctly done, and to mitigate the potential inflation of Obj.magic, I've added a few simplification rules to avoid redundant magics, push them down inside terms, favor the form (Obj.magic f x y z), etc.
| * Proof using: do not clear unused section hyps automaticallyGravatar Enrico Tassi2015-12-15
| | | | | | | | | | | | The option is still there, but not documented since it is too dangerous. Hints and type classes instances are not taking cleared variables into account.
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-24 17:54:59 +0000