diff options
Diffstat (limited to 'plugins/romega')
| -rw-r--r-- | plugins/romega/const_omega.ml | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index 689462704..3fa9e02cf 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -210,10 +210,15 @@ let rec mk_nat = function (* Lists *) -let mkListConst c u = - Term.mkConstructU (Globnames.destConstructRef - (Coqlib.gen_reference "" ["Init";"Datatypes"] c), - Univ.Instance.of_array [|u|]) +let mkListConst c = + let r = + Coqlib.gen_reference "" ["Init";"Datatypes"] c + in + let inst = + if Global.is_polymorphic r then fun u -> Univ.Instance.of_array [|u|] + else fun _ -> Univ.Instance.empty + in + fun u -> Term.mkConstructU (Globnames.destConstructRef r, inst u) let coq_cons univ typ = Term.mkApp (mkListConst "cons" univ, [|typ|]) let coq_nil univ typ = Term.mkApp (mkListConst "nil" univ, [|typ|]) |