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 | |
| 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')
| -rw-r--r-- | intf/glob_term.mli | 1 | ||||
| -rw-r--r-- | intf/notation_term.mli | 1 |
2 files changed, 0 insertions, 2 deletions
diff --git a/intf/glob_term.mli b/intf/glob_term.mli index 237d033662..832ee4e4b0 100644 --- a/intf/glob_term.mli +++ b/intf/glob_term.mli @@ -41,7 +41,6 @@ type glob_constr = | GCases of Loc.t * case_style * glob_constr option * tomatch_tuples * cases_clauses (** [GCases(l,style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in [MatchStyle]) *) - | GProj of Loc.t * projection * glob_constr | GLetTuple of Loc.t * Name.t list * (Name.t * glob_constr option) * glob_constr * glob_constr | GIf of Loc.t * glob_constr * (Name.t * glob_constr option) * glob_constr * glob_constr 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 |