aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2015-12-21Finer-grained types for toplevel values.Pierre-Marie Pédrot
2015-12-21Removing 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-21Sharing 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-21Changing the toplevel type of the int_or_var generic type to int.Pierre-Marie Pédrot
2015-12-21Removing the now useless genarg generic argument.Pierre-Marie Pédrot
2015-12-21Using dynamic values in tactic evaluation.Pierre-Marie Pédrot
2015-12-21Attaching a dynamic argument to the toplevel type of generic arguments.Pierre-Marie Pédrot
2015-12-21Trust 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-18COMMENTS: added to the "Constr.case_info" type.Matej Kosik
2015-12-18CLEANUP: the definition of the "Constrexpr.case_expr" type was simplifiedMatej Kosik
2015-12-18CLEANUP: removing unnecessary aliasMatej Kosik
2015-12-18CLEANUP: Vernacexpr.VernacDeclareTacticDefinitionMatej 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-18TYPOGRAPHY: correction of one particular error in the Reference ManualMatej Kosik
2015-12-18CLEANUP: Removing "Vernacexpr.VernacNop" variant to which no Vernacular ↵Matej Kosik
command is mapped.
2015-12-18CLEANUP: simplifying "Coqtop.init_gc" implementationMatej Kosik
2015-12-18CLEANUP: removing unnecessary wrapper functionMatej Kosik
2015-12-18COMMENTS: added to some variants of "Globalnames.global_reference" type.Matej Kosik
2015-12-18COMMENTS: added to some variants of "Misctypes.glob_sort_gen" type.Matej Kosik
2015-12-18COMMENTS: added to some variants of "Glob_term.glob_constr" type.Matej Kosik
2015-12-18COMMENTS: added to some variants of the "Constrexpr.prim_token" type.Matej Kosik
2015-12-18ALPHA-CONVERSION: in "parsing/g_vernac.ml4" fileMatej Kosik
2015-12-18COMMENTS: added to the "Unicode" module.Matej Kosik
2015-12-18COMMENTS: updated in the "Option" module.Matej Kosik
2015-12-18COMMENTS: added to some variants of the "Constr.kind_of_term" type.Matej Kosik
2015-12-18CLEANUP: Vernacexpr.vernac_exprMatej 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-18COMMENTS: added to the "Predicate" moduleMatej 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-18COMMENTS: added to the "Names" module.Matej Kosik
2015-12-18Tying the loop in tactic printing API.Pierre-Marie Pédrot
2015-12-17Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-17ALPHA-CONVERSION: in the "Reduction" module: clos_fconv --> clos_gen_convMatej Kosik
2015-12-17ALPHA-CONVERSION: in the "Reduction" module: fconv --> gen_convMatej Kosik
2015-12-17CLEANUP: in the Reduction moduleMatej Kosik
2015-12-17CLEANUP: in the Reductionops moduleMatej Kosik
2015-12-17CLEANUP: in the Reduction moduleMatej Kosik
2015-12-17Getting rid of some hardwired generic arguments.Pierre-Marie Pédrot
2015-12-16Updating credits.Hugo Herbelin
2015-12-16Update version numbers and magic numbers for 8.5rc1 release.Maxime Dénès
2015-12-16FIx parsing of tactic "simple refine".Maxime Dénès
2015-12-16Add a "simple refine" variant of "refine" that does not call "shelve_unifiable".Guillaume Melquiond
2015-12-16Extraction: slightly better heuristic for Obj.magic simplificationsPierre Letouzey
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.
2015-12-16Extraction: fixed beta-red with Obj.magic (#2795 again) + other simplificationsPierre Letouzey
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.
2015-12-15Proof using: do not clear unused section hyps automaticallyEnrico Tassi
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.
2015-12-15Fix test suite after change in extraction.Maxime Dénès
2015-12-15Extraction: more cautious use of intermediate result caching (fix #3923)Pierre Letouzey
During an extraction, a few tables are maintained to cache intermediate results. Due to modules, the kernel_name index for these caching tables aren't enough. For instance, in bug #3923, a constant is first transparent (from inside the module) then opaque (when seen from the signature). The previous protections were actually obsolete (tests via visible_con), we now checks that the constant_body is still the same.
2015-12-15Fix test-suite files after change in refine tactic.Maxime Dénès
Change was introduced by cedcfc9bc386456f3fdd225f739706e4f7a2902c.
2015-12-15Extraction: fix a few little glitches with my last commit (replacing unused ↵Pierre Letouzey
vars by _)
2015-12-15Fixing e3cefca41b about supposingly simplifying primitive projectionsHugo Herbelin
typing. Had built the instance for substitution in the wrong context.
2015-12-15Fixing unexpected length of context in a typing function, detected byHugo Herbelin
cleaning done in e8c47b652a0. It had no serious consequences except having whd-reduction blocked on a let-in when typing a return clause with let-ins in the arity (a priori resulting in return types of the form e.g. "(let x:=t in fun y => T) u" instead of T[x:=t;y:=u], if I'm not mistaking). This fixes 3210.v in test-suite.
2015-12-15Adding a test for the unshelve tactical.Pierre-Marie Pédrot
2015-12-15Refine tactic now shelves unifiable holes.Pierre-Marie Pédrot
The unshelve tactical can be used to get the shelved holes. This changes the proper ordering of holes though, so expect some broken scripts. Also, the test-suite is not fixed yet.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 04:56:15 +0000