aboutsummaryrefslogtreecommitdiff
path: root/tactics/taccoerce.ml
AgeCommit message (Expand)Author
2016-08-19Moving Taccoerce to ltac/ folder.Pierre-Marie Pédrot
2016-06-16Merge PR #100: fresh now accepts more things than just identifiers.Pierre-Marie Pédrot
2016-05-04Normalizing the names of dynamic types to follow a typ_* scheme.Pierre-Marie Pédrot
2016-05-04Removing the Value.of_* API for parameterized types.Pierre-Marie Pédrot
2016-05-04Moving the Val module to Geninterp.Pierre-Marie Pédrot
2016-05-04Switching to an untyped toplevel representation for Ltac values.Pierre-Marie Pédrot
2016-04-15Merge remote-tracking branch 'OFFICIAL/trunk' into morefreshPierre Courtieu
2016-03-17Removing the registering of default values for generic arguments.Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-12Adding support for fresh for meta's and evar's.Pierre Courtieu
2015-12-21Finer-grained types for toplevel values.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-09-10fresh now accepts more things than just identifiers.Pierre Courtieu
2015-02-12Fixing compilation for 3.12.Pierre-Marie Pédrot
2015-02-12Tentative fix for bug #4027.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-09-01Moving the decompose tactic out of the AST.Pierre-Marie Pédrot
2014-08-29Type-safe version of genarg list / pair / opt functions.Pierre-Marie Pédrot
2014-08-18Reorganisation of intropattern codeHugo Herbelin
2014-08-06[uconstr]: use a closure instead of eager substitution.Arnaud Spiwack
2014-08-06Removing "intros untils" from the AST.Pierre-Marie Pédrot
2014-08-01Faster uconstr.Arnaud Spiwack
2014-08-01Untyped terms in ltac: simplify [coerce_to_uconstr].Arnaud Spiwack
2014-07-29Untyped terms in tactic: add the possibility to use a typed term inside an un...Arnaud Spiwack
2014-07-29Add a type of untyped term to Ltac's value.Arnaud Spiwack
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2013-10-24More monomorphic List.mem + List.assoc + ...letouzey
2013-07-05Expurgating the useless difference between List0 and List1 at theppedrot
2013-06-27Removed the distinction between generic Ltac vars and Let/Introppedrot
2013-06-21Cutting the dependency of Genarg in constr_expr, glob_constrppedrot
2013-06-19Moving wit_unit to Stdarg.ppedrot
2013-06-18Proof-of-concept: moved four easy-to-handle generic arguments toppedrot
2013-06-13Normalizing exception raised by tactic coercions.ppedrot
2013-06-12Moving coercion functions out of Tacinterp.ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 05:46:34 +0000