diff options
Diffstat (limited to 'pretyping/evardefine.ml')
| -rw-r--r-- | pretyping/evardefine.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index c5ae684e3..c2b267dd8 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -181,7 +181,7 @@ let define_evar_as_sort env evd (ev,args) = constraint on its domain and codomain. If the input constraint is an evar instantiate it with the product of 2 new evars. *) -let split_tycon loc env evd tycon = +let split_tycon ?loc env evd tycon = let rec real_split evd c = let t = Reductionops.whd_all env evd c in match EConstr.kind evd t with @@ -193,7 +193,7 @@ let split_tycon loc env evd tycon = | App (c,args) when isEvar evd c -> let (evd',lam) = define_evar_as_lambda env evd (destEvar evd c) in real_split evd' (mkApp (lam,args)) - | _ -> error_not_product ~loc env evd c + | _ -> error_not_product ?loc env evd c in match tycon with | None -> evd,(Anonymous,None,None) |