diff options
| author | Hugo Herbelin | 2018-11-13 15:42:02 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-06-01 14:54:54 +0200 |
| commit | 45352e43db4c67eab23517f13e94ba1b5cc11808 (patch) | |
| tree | 7812917af30d62fa8edcb4e85a89c1ed4a3ec65e /plugins/funind | |
| parent | 7032085c809993d6a173e51aec447c02828ae070 (diff) | |
Towards unifying parsing/printing for universe instances and Type's argument.
We consistently use:
- UUnknown: to mean a rigid anonymous universe
(written Type in instances and Type as a sort)
[was formerly encoded as [] in Type's argument]
- UAnonymous: to mean a flexible anonymous universe
(written _ in instances and Type@{_} as a sort)
[was formerly encoded as [None] in Type's argument]
- UNamed: to mean a named universe or universe expression
(written id or qualid in instances and Type@{id} or Type@{qualid} or more
generally Type@{id+n}, Type@{qualid+n}, Type@{max(...)} as a sort)
There is a little change of syntax: "_" in a "max" list of universes
(e.g. "Type@{max(_,id+1)}" is not anymore allowed. But it was
trivially satisfiable by unifying the flexible universe with a
neighbor of the list and the syntax is anyway not documented.
There is a little change of semantics: if I do id@{Type} for an
abbreviation "id := Type", it will consider a rigid variable rather
than a flexible variable as before.
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 4c67d65816..889a2d7359 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1302,7 +1302,7 @@ let rec rebuild_return_type rt = CAst.make ?loc @@ Constrexpr.CLetIn(na,v,t,rebuild_return_type t') | _ -> CAst.make ?loc @@ Constrexpr.CProdN([Constrexpr.CLocalAssum ([CAst.make Anonymous], Constrexpr.Default Decl_kinds.Explicit, rt)], - CAst.make @@ Constrexpr.CSort(GType [])) + CAst.make @@ Constrexpr.CSort(GType UUnknown)) let do_build_inductive evd (funconstants: pconstant list) (funsargs: (Name.t * glob_constr * glob_constr option) list list) |