aboutsummaryrefslogtreecommitdiff
path: root/intf/constrexpr.mli
AgeCommit message (Expand)Author
2017-06-07Put all plugins behind an "API".Matej Kosik
2017-05-24[location] Renaming "CAst.ast" to "CAst.t"Matej Košík
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-05-15[interp] [ast] Make raw_cases_pattern_expr private.Emilio Jesus Gallego Arias
2017-04-25[location] [ast] Port module AST to CAstEmilio Jesus Gallego Arias
2017-04-25[location] [ast] Switch Constrexpr AST to an extensible node type.Emilio Jesus Gallego Arias
2017-04-25[location] Be consistent with type module qualificationEmilio Jesus Gallego Arias
2017-04-24[location] More located use.Emilio Jesus Gallego Arias
2017-04-24[location] Use Loc.located for constr_expr.Emilio Jesus Gallego Arias
2017-04-24[constrexpr] Make patterns use Loc.located for location informationEmilio Jesus Gallego Arias
2017-04-09Documenting how the recursive indices of a fixpoint are computed.Hugo Herbelin
2017-03-24Replacing "cast surgery" in LetIn by a proper field (see PR #404).Hugo Herbelin
2017-03-24Unifying standard "constr_level" names for constructors of local_binder_expr.Hugo Herbelin
2017-03-24Renaming local_binder into local_binder_expr.Hugo Herbelin
2017-03-24Standardized the order of constructors for binders: Assum then Def.Hugo Herbelin
2017-03-24"Standardizing" the name LocalPatten into LocalRawPattern.Hugo Herbelin
2016-09-22Revert "Merge remote-tracking branch 'github/pr/283' into trunk"Maxime Dénès
2016-09-20Rename Decl_kinds.binding_kind into Decls_kind.implicit_status.Maxime Dénès
2016-06-27Adding ability to put any pattern in binders, prefixed by a quote.Daniel de Rauglaudre
2016-03-13Adopting the same rules for interpreting @, abbreviations andHugo Herbelin
2016-03-13Supporting "(@foo) args" in patterns, where "@foo" has no arguments.Hugo Herbelin
2016-01-29Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-23Implement support for universe binder lists in Instance and Program Fixpoint/...Matthieu Sozeau
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-11COMMENTS: added to the "Constrexpr.CCases" variant.Matej Kosik
2016-01-11CLEANUP: removing unused fieldMatej Kosik
2015-12-18CLEANUP: the definition of the "Constrexpr.case_expr" type was simplifiedMatej Kosik
2015-12-18COMMENTS: added to some variants of the "Constrexpr.prim_token" type.Matej Kosik
2015-01-12Update headers.Maxime Dénès
2014-09-30Add syntax for naming new goals in refine: writing ?[id] instead of _Hugo Herbelin
2014-09-12Parsing evar instances.Hugo Herbelin
2014-09-12Referring to evars by names. Added a parser for evars (but parsing ofHugo Herbelin
2014-09-08Parsing of Type@{max(i,j)}.Matthieu Sozeau
2014-06-04- Fix hashing of levels to get the "right" order in universe contexts etc...Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2013-11-27Adding generic solvers to term holes. For now, no resolution mechanism norPierre-Marie Pédrot
2012-12-18Modulification of nameppedrot
2012-12-14Modulification of identifierppedrot
2012-12-14Implemented a full-fledged equality on [constr_expr]. By the way,ppedrot
2012-10-02avoid referring to Term in constrexpr.mli and glob_term.mliletouzey
2012-08-08Updating headers.herbelin
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-06-14Internalization of pattern is done in two phases.pboutill
2012-05-29New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstrletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 03:30:50 +0000