aboutsummaryrefslogtreecommitdiff
path: root/interp/topconstr.mli
AgeCommit message (Expand)Author
2018-05-30[api] Remove deprecated objects in engine / interp / libraryEmilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-22[ast] Improve precision of Ast location recognition in serialization.Emilio Jesus Gallego Arias
2017-11-19[parser] Remove unnecessary statically initialized hook.Emilio Jesus Gallego Arias
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-04-25[location] Make location optional in Loc.locatedEmilio Jesus Gallego Arias
2017-03-24Renaming local_binder into local_binder_expr.Hugo Herbelin
2016-09-21Fix an error-prone error API.Pierre-Marie Pédrot
2016-08-19Unify location handling of error functions.Emilio Jesus Gallego Arias
2016-04-27Reformatting + removal of some useless data + some cut-eliminationHugo Herbelin
2016-03-12A more explicit name to the asymmetric boolean flag.Hugo Herbelin
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2013-09-02Removing more association lists in Constrintern.ppedrot
2013-03-13Modules and ppvernac, sequel of Enrico's commit 16261letouzey
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-29remove many excessive open Util & Errors in mli'sletouzey
2012-05-29Basic stuff about constr_expr migrated from topconstr to constrexpr_opsletouzey
2012-05-29Stuff about notation_constr (ex-aconstr) now in notation_ops.mlletouzey
2012-05-29New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstrletouzey
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
2012-05-29Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evdletouzey
2012-05-15Notations are back in the "in" clause of pattern matching.pboutill
2012-04-12"A -> B" is a notation for "forall _ : A, B".pboutill
2012-03-20Fixing bug #2724 (using notations with binders in cases patternsherbelin
2012-03-02Glob_term.predicate_pattern: No number of parameters with letins.pboutill
2012-03-02Noise for nothingpboutill
2012-02-29In the syntax of pattern matching, "in" clauses are patterns.pboutill
2012-01-19Boolean Option Patterns Compatibilitypboutill
2012-01-16Parameters in pattern first step.pboutill
2011-10-28Remove dynamic stuff from constr_expr and glob_constrglondu
2011-08-30Quick improvement of some error messages related to module applicationherbelin
2011-07-22Add a syntax entry for fully applied constructor patternpboutill
2011-06-12Rather quick hack to avoid using notations involving "Type" whenherbelin
2011-02-11Annotations at functor applications:letouzey
2011-01-31A fine-grain control of inlining at functor application via priority levelsletouzey
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
2010-07-22Extension of the recursive notations mechanismherbelin
2010-07-22Constrintern: unified push_name_env and push_loc_name_env; madeherbelin
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-06-14Added printing of recursive notations in cases pattern (supported by wish 2248).herbelin
2010-06-08Fix treatment of {struct x} annotations in presence of generalizedmsozeau
2010-04-29Various minor improvements of comments in mli for ocamldocletouzey
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:08:19 +0000