diff options
Diffstat (limited to 'pretyping/evardefine.ml')
| -rw-r--r-- | pretyping/evardefine.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index 5f12f360b..18dbbea1b 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -10,6 +10,7 @@ open Util open Pp open Names open Term +open Constr open Termops open EConstr open Vars @@ -82,7 +83,7 @@ let define_pure_evar_as_product evd evk = let newenv = push_named (LocalAssum (id, dom)) evenv in let src = evar_source evk evd1 in let filter = Filter.extend 1 (evar_filter evi) in - if is_prop_sort (ESorts.kind evd1 s) then + if Sorts.is_prop (ESorts.kind evd1 s) then (* Impredicative product, conclusion must fall in [Prop]. *) new_evar newenv evd1 concl ~src ~filter else |