aboutsummaryrefslogtreecommitdiff
path: root/pretyping/pretyping.mli
AgeCommit message (Expand)Author
2017-02-14Ltac now uses evar-based constrs.Pierre-Marie Pédrot
2017-02-14Making judgment type generic over the type of inner constrs.Pierre-Marie Pédrot
2017-02-14Pretyping API using EConstr.Pierre-Marie Pédrot
2016-11-18Merge branch 'v8.6'Pierre-Marie Pédrot
2016-11-07More explicit name for status of unification constraints.Maxime Dénès
2016-10-02Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-28Fix bug #4723 and FIXME in API for solve_by_tacMatthieu Sozeau
2016-09-15Untangling Tacexpr from lower strata.Pierre-Marie Pédrot
2016-09-08Unplugging Tacexpr in several interface files.Pierre-Marie Pédrot
2016-06-18Moving the typing_flags to the environment.Pierre-Marie Pédrot
2016-06-16Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Pierre-Marie Pédrot
2016-06-15Allow `Pretyping.search_guard` to not check guardArnaud Spiwack
2016-05-04Moving the Val module to Geninterp.Pierre-Marie Pédrot
2016-03-25Moving type_uconstr to Pretyping.Pierre-Marie Pédrot
2016-03-20Making Evarutil independent from Reductionops.Pierre-Marie Pédrot
2016-02-19Adding location to universes generated by the pretyper.Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-12-21Using dynamic values in tactic evaluation.Pierre-Marie Pédrot
2015-12-04Removing dynamic inclusion of constrs in tactic AST.Pierre-Marie Pédrot
2015-10-26Documenting a bit more interpretation functions in passing.Hugo Herbelin
2015-08-02Fixing #4221 (interpreting bound variables using ltac env was possiblyHugo Herbelin
2015-02-23Fix some typos in comments.Guillaume Melquiond
2015-01-12Update headers.Maxime Dénès
2014-10-25This commit introduces changes in induction and destruct.Hugo Herbelin
2014-09-12Uniformisation of the order of arguments env and sigma.Hugo Herbelin
2014-09-05Adds an identifier context in pretying's Ltac context.Arnaud Spiwack
2014-08-07Better structure for Ltac pretyping environments.Pierre-Marie Pédrot
2014-08-06[uconstr]: use a closure instead of eager substitution.Arnaud Spiwack
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
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
2014-02-12TC: honor the use_typeclasses flag in pretypingEnrico Tassi
2013-11-27Adding generic solvers to term holes. For now, no resolution mechanism norPierre-Marie Pédrot
2013-06-24Using the whole tactic environment while Pretyping.ppedrot
2013-06-22Generalizing the use of maps instead of lists in the interpretationppedrot
2013-05-09A uniformization step around understand_* and interp_* functions.herbelin
2013-04-29Merging Context and Sign.ppedrot
2012-12-14Modulification of identifierppedrot
2012-08-08Updating headers.herbelin
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
2012-03-14Revise API of understand_ltac to be parameterized by a flag for resolution of...msozeau
2012-03-14Second step of integration of Program:msozeau
2012-03-02Noise for nothingpboutill
2011-09-26Moving implicit tactic support from Tacinterp to Pfedit and final evarherbelin
2010-12-24More {raw => glob} changes for consistencyglondu
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-12-23Change of nomenclature: rawconstr -> glob_constrglondu
2010-07-24Updated all headers for 8.3 and trunkherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 15:31:53 +0000