aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/notation_ops.mli
Commit message (Collapse)AuthorAge
* [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
| | | | Now it is a private field, locations are optional.
* Using the same type of binders for interning and externing.Gravatar Hugo Herbelin2017-03-24
| | | | | | Previously a union type was used for externing. In particular, moving extended_glob_local_binder to glob_constr.ml.
* Quick fix to #4595 (making notations containing "ltac:" unused for printing).Gravatar Hugo Herbelin2016-10-04
| | | | Also getting rid of a global side-effect.
* Warning about similar notations now up to alpha-conversion.Gravatar Hugo Herbelin2016-09-28
| | | | | | | | | | This allows to define on purpose the very same notation in different files, as currently the notations for *, +, - in Nat.v and Peano.v (with the first one using variables n and m and the second one using the default variables used by Infix, namely x and y). This makes also the "notation-overridden" warning less enigmatic facing two notations which are the same up to the choice of names.
* removing ocamldoc-related syntax errorsGravatar Matej Kosik2016-07-12
|
* Adding ability to put any pattern in binders, prefixed by a quote.Gravatar Daniel de Rauglaudre2016-06-27
| | | | Cf CHANGES for details.
* A slight phase of documentation and uniformization of names ofGravatar Hugo Herbelin2016-06-02
| | | | | | | | | | | | | | | | | | | | | functions about interpretation, internalization, externalization of notations. Main syntactic changes: - subst_aconstr_in_glob_constr -> instantiate_notation_constr (because aconstr has been renamed to notation_constr long time ago) - extern_symbol -> extern_notation (because symbol.ml has been renamed to notation.ml long time ago) - documentation of notations_ops.mli Main semantic changes: - Notation_ops.eq_glob_constr which was partial eq disappears: use glob_constr_eq instead - In particular, this impacts a change on funind which now use the (fully implemented) glob_constr_eq Somehow, instantiate_notation_constr should be in notation_ops.ml for symmetry with match_notation_constr but it is bit painful to do.
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
|
* Fixing equality of notation_constrs. Fixes bug #4136.Gravatar Pierre-Marie Pédrot2015-03-24
|
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
| | | | | | | | With ocaml 4.01, the 'unused open' warning also checks the mli :-) Beware: some open are reported as useless when compiling with camlp5, but are necessary for compatibility with camlp4. These open are now marked with a comment.
* Notations can now accept dummy arguments. If ever a bound variable is notGravatar Pierre-Marie Pédrot2013-12-22
| | | | | | used, they are automatically flagged as only parsing. CAVEAT: unused arguments are not typechecked, because they are dropped before the interpretation phase.
* Replacing uses of association lists by maps in notations.Gravatar ppedrot2013-08-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16655 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modulification of nameGravatar ppedrot2012-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16099 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modulification of identifierGravatar ppedrot2012-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a constr_pattern_eqGravatar ppedrot2012-11-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15995 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updating headers.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixup implicits in patterns & notationsGravatar pboutill2012-07-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15633 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
| | | | | | | | | | were closed (i.e. the only remaining ones are those of printing/parsing). Meanwhile, a simplified interface is provided in loc.mli. This also permits to put Pp in Clib, because it does not depend on CAMLP4/5 anymore. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15475 85f007b7-540e-0410-9357-904b9bb8a0f7
* remove many excessive open Util & Errors in mli'sGravatar letouzey2012-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15392 85f007b7-540e-0410-9357-904b9bb8a0f7
* Stuff about notation_constr (ex-aconstr) now in notation_ops.mlGravatar letouzey2012-05-29
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15381 85f007b7-540e-0410-9357-904b9bb8a0f7