diff options
Diffstat (limited to 'vernac/record.ml')
| -rw-r--r-- | vernac/record.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/record.ml b/vernac/record.ml index 7dd70d0133..d61f44cac8 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -124,7 +124,7 @@ let typecheck_params_and_fields finite def id pl t ps nots fs = let s' = EConstr.ESorts.kind !evars s' in (if poly then match Evd.is_sort_variable !evars s' with - | Some l -> evars := Evd.make_flexible_variable !evars true l; + | Some l -> evars := Evd.make_flexible_variable !evars ~algebraic:true l; s, s', true | None -> s, s', false else s, s', false) |