aboutsummaryrefslogtreecommitdiff
path: root/interp/constrextern.ml
AgeCommit message (Expand)Author
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-06-19Fixing printing of @f with no argumentsherbelin
2012-06-14Constrextern is allow to use partially applied notationspboutill
2012-06-14Internalization of pattern is done in two phases.pboutill
2012-05-29No more Univ in grammar.cmaletouzey
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
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-03-26Fixing deactivation of scope at printing time in the body of aherbelin
2012-03-20Fixing alpha-conversion bug #2723 introduced in r12485-12486.herbelin
2012-03-02Glob_term.predicate_pattern: No number of parameters with letins.pboutill
2012-03-02"Let in" in pattern hell, one more iterationpboutill
2012-03-02Noise for nothingpboutill
2012-02-29In the syntax of pattern matching, "in" clauses are patterns.pboutill
2012-02-01Debugger vs tracer: Two different behaviors wrt printing: The debuggerherbelin
2012-01-27Printing bugs with match patterns:herbelin
2012-01-20Added new command "Set Parsing Explicit" for deactivating parsing (andherbelin
2012-01-19Boolean Option Patterns Compatibilitypboutill
2012-01-16Parameters in pattern first step.pboutill
2011-11-07Allow "|_=>_" in "match" in patterns, no more forced enumeration of constructorsletouzey
2011-10-28Remove dynamic stuff from constr_expr and glob_constrglondu
2011-08-10Fixing printing bug with last trailing non-maximally implicitherbelin
2011-07-26Partial revert of r14292pboutill
2011-07-22Add a syntax entry for fully applied constructor patternpboutill
2011-07-16This adds two option tables 'Printing Record' and 'Printing Constructor'herbelin
2011-07-16This option disables the use of the '{| field := ... |}' notationherbelin
2011-06-12Rather quick hack to avoid using notations involving "Type" whenherbelin
2011-04-24Yet another bug in printing fix with let-in bindersherbelin
2011-04-08Fixing multiple printing bugs with "Notation f x := ..."herbelin
2011-03-31Did that adding a rule for printing applications as "f(x)" works.herbelin
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-10-03Added multiple implicit arguments rules per name.herbelin
2010-09-28Fix function applications without labels (OCaml warning 6)glondu
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
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-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-18Fixed some printing bugs.herbelin
2010-04-10Optimized need for delimiters when disjoint scopes for strings andherbelin
2010-01-06Allowed handling of partly-applied record constructors. (Fix for bug #2196.)gmelquio
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 15:15:09 +0000