aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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.
2015-12-15Fixing e7f7fc3e058 (wrong chop on contexts). This fixes test-suite.Hugo Herbelin
2015-12-15API: documenting context_chop and removing a duplicate.Hugo Herbelin
2015-12-15Changing the order of the goals generated by unshelve.Pierre-Marie Pédrot
2015-12-15Adding a token "index" representing positions (1st, 2nd, etc.).Hugo Herbelin
2015-12-15Simplifying documentation of "assert form as pat".Hugo Herbelin
2015-12-15Granting clear_flag in injection, even legacy mode. This is possibleHugo Herbelin
since the clear_flag is new.
2015-12-15Tactics: Generalizing the use of the experimental clearing modifier toHugo Herbelin
all cases of rewrite.
2015-12-15Extraction: replace unused variable names by _ in funs and matchs (fix #2842)Pierre Letouzey
This is done via a unique pass which seems roughly linear in practice, even on big developments like CompCert. There's a List.nth in an env at each MLrel, that could be made logarithmic if necessary via Okasaki's skew list for instance. Another approach would be to keep names (as a form of documentation), but prefix them by _ to please OCaml's warnings. For now, let's be radical and use the _ pattern.
2015-12-15Revert "Revert PMP's fix of #2498, which introduces an incompatibility with ↵Pierre-Marie Pédrot
lablgtk" This reverts commit 469cb750c6c1aa46f77b2a89a36f79f29aa97073.
2015-12-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-14Extraction: allow basic beta-reduction even through a MLmagic (fix #2795)Pierre Letouzey
This fix only handles MLapp(MLmagic(MLlam...),...). Someday, we'll have to properly investigate the interaction between all the other optimizations and MLmagic. But well, at least this precise bug is fixed now.
2015-12-14Fixing little bug of coq_makefile with unterminated comment.Hugo Herbelin
Force failing when reaching end of file with unterminated comment when parsing Make (project) file.
2015-12-14extraction_impl.v: fix a typoPierre Letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-12 06:49:07 +0000