diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-01-24 16:45:46 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-01-30 14:19:57 +0100 |
| commit | de988641848ecb26f749fbc3f50ce9194db46a4c (patch) | |
| tree | 7eb76c35fb7c4543f91405266d54523026403c54 /plugins/funind/indfun.ml | |
| parent | 879ebad4d0b39fda275a72ba44c1f4dfbb9282e5 (diff) | |
Use r.(p) syntax to print primitive projections.
There is no way today to distinguish primitive projections from
compatibility constants, at least in the case of a record without
parameters.
We remedy to this by always using the r.(p) syntax when printing
primitive projections, even with Set Printing All.
The input syntax r.(p) is still elaborated to GApp, so that we can preserve
the compatibility layer. Hopefully we can make up a plan to get rid of that
layer, but it will require fixing a few problems.
Diffstat (limited to 'plugins/funind/indfun.ml')
| -rw-r--r-- | plugins/funind/indfun.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 071bab2f3..58154d310 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -215,6 +215,7 @@ let is_rec names = | GCases(_,_,el,brl) -> List.exists (fun (e,_) -> lookup names e) el || List.exists (lookup_br names) brl + | GProj(_,c) -> lookup names c and lookup_br names (_,(idl,_,rt)) = let new_names = List.fold_right Id.Set.remove idl names in lookup new_names rt @@ -779,6 +780,7 @@ let rec add_args id new_args = CAst.map (function | CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation.") | CGeneralization _ -> anomaly ~label:"add_args " (Pp.str "CGeneralization.") | CDelimiters _ -> anomaly ~label:"add_args " (Pp.str "CDelimiters.") + | CProj _ -> user_err Pp.(str "Funind does not support primitive projections") ) exception Stop of Constrexpr.constr_expr |