aboutsummaryrefslogtreecommitdiff
path: root/interp/topconstr.ml
AgeCommit message (Expand)Author
2012-12-14Modulification of identifierppedrot
2012-11-25Monomorphization (interp)ppedrot
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
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-06-04Replacing some str with strbrkppedrot
2012-05-30More uniformisation in Pp.warn functions.ppedrot
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-29Glob_term now mli-only, operations now in Glob_opsletouzey
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-04-06Fixing a few bugs (see #2571) related to interpretation of multiple bindersherbelin
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-20Notations with binders: Accepting using notations for functional termsherbelin
2012-01-19Boolean Option Patterns Compatibilitypboutill
2012-01-16Parameters in pattern first step.pboutill
2011-12-16Fixing amazing loop when using eta-expansion in pattern-matching forherbelin
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-06-08Make Notation works with anonymous-level "Type".herbelin
2011-04-15Take benefit of eta-expansion so that "ex P" is displayed "exists x, P x".herbelin
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-12-04Fixing bug #2448 (wrongly-scoped alpha-renaming in notations).herbelin
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-07-29Fixed a bug introduced (r13316/r13329) in the printing of notationsherbelin
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-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-29Remove the svn-specific $Id$ annotationsletouzey
2010-03-29Several bug-fixes and improvements of coqdocherbelin
2010-01-17Variant !F M for functor application that does not honor the Inline declarationsletouzey
2010-01-07Include can accept both Module and Module Typeletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 08:06:58 +0000