diff options
| author | Maxime Dénès | 2018-02-12 09:59:16 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-02-12 09:59:16 +0100 |
| commit | 4fb4f1adf18648b4fb561986379e033b00423148 (patch) | |
| tree | 876f561f9310b9e15f3ac20ca71f9dd28f90b157 /interp/constrintern.ml | |
| parent | 349944eb8e3abd51dc2b94051a887253a2ae9198 (diff) | |
| parent | de988641848ecb26f749fbc3f50ce9194db46a4c (diff) | |
Merge PR #6651: Use r.(p) syntax to print primitive projections.
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 61b33aa415..8e99435dbc 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1869,7 +1869,13 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = | CCast (c1, c2) -> DAst.make ?loc @@ GCast (intern env c1, Miscops.map_cast_type (intern_type env) c2) - ) + | CProj (pr, c) -> + match intern_reference pr with + | ConstRef p -> + DAst.make ?loc @@ GProj (Projection.make p false, intern env c) + | _ -> + raise (InternalizationError (loc,IllegalMetavariable)) (* FIXME *) + ) and intern_type env = intern (set_type_scope env) and intern_local_binder env bind : intern_env * Glob_term.extended_glob_local_binder list = |