diff options
| author | Matthieu Sozeau | 2014-09-17 00:03:46 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-09-17 00:10:03 +0200 |
| commit | c5ecebf6fefbaa673dda506175a2aa4a69d79807 (patch) | |
| tree | e364fd928f247c249767ffb679b0265857327a6a /intf/notation_term.mli | |
| parent | 4dc8746cac24ba72a1ec4dfa764a1ae88ce79277 (diff) | |
Revert specific syntax for primitive projections, avoiding ugly
contortions in internalization/externalization. It uses a fully typed
version of detyping, requiring the environment, to move from
primitive projection applications to regular applications of
the eta-expanded version. The kernel is unchanged, and only
constrMatching needs compatibility code now.
Diffstat (limited to 'intf/notation_term.mli')
| -rw-r--r-- | intf/notation_term.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/intf/notation_term.mli b/intf/notation_term.mli index 8bb43e96a5..daf605ab28 100644 --- a/intf/notation_term.mli +++ b/intf/notation_term.mli @@ -25,7 +25,6 @@ type notation_constr = | NVar of Id.t | NApp of notation_constr * notation_constr list | NHole of Evar_kinds.t * Genarg.glob_generic_argument option - | NProj of projection * notation_constr | NList of Id.t * Id.t * notation_constr * notation_constr * bool (** Part only in [glob_constr] *) | NLambda of Name.t * notation_constr * notation_constr |