| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-12-28 | Implementing non-focussed generic arguments. | Pierre-Marie Pédrot | |
| Kind of enhances the situation of bug #4409. Now arguments can be interpreted globally or focussedly in a dynamic fashion because the interpretation function returns a Ftactic.t. The bug is not fixed yet because we should tweak the interpretation of tactic arguments. | |||
| 2015-12-28 | Removing the special status of open_constr generic argument. | Pierre-Marie Pédrot | |
| We also intepret it at toplevel as a true constr and push the resulting evarmap in the current state. | |||
| 2015-12-28 | Eradicating uses of open_constr in TACTIC EXTEND in favour of uconstr. | Pierre-Marie Pédrot | |
| 2015-12-27 | Factorizing code for untyped constr evaluation. | Pierre-Marie Pédrot | |
| 2015-12-27 | Removing dead code. | Pierre-Marie Pédrot | |
| 2015-12-27 | Tentative API fix for tactic arguments to be fed to tclWITHHOLES. | Pierre-Marie Pédrot | |
| The previous implementation was a source of evar leaks if misused, as it created values coming together with their current evar_map. This is dead wrong if the value is not used on the spot. To fix this, we rather return a ['a delayed_open] object. Two argument types were modified: bindings and constr_bindings. The open_constr argument should also be fixed, but it is more entangled and thus I leave it for another commit. | |||
| 2015-12-25 | Moving basic generalization tactics upwards for possible use in "intros". | Hugo Herbelin | |
| 2015-12-25 | Moving code of specialize so that it can accept "as" (no semantic change). | Hugo Herbelin | |
| 2015-12-25 | Moving specialize to Proofview.tactic. | Hugo Herbelin | |
| 2015-12-25 | Fixing a bug in the order of side conditions for introduction pattern -> and <-. | Hugo Herbelin | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |