diff options
| author | Pierre-Marie Pédrot | 2016-09-08 14:56:33 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-09-08 15:41:16 +0200 |
| commit | 13266ce4c37cb648b5e4e391aa5d7486bbcdb4ee (patch) | |
| tree | f76fd37023c71c20520e34e4a51c487e7a0388a0 /pretyping/evardefine.ml | |
| parent | 79e7a0de25bcb2f10a7f3d1960a8f16eefdbb5a6 (diff) | |
| parent | fc579fdc83b751a44a18d2373e86ab38806e7306 (diff) | |
Merge PR #244.
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 29eb00c617..06f619410c 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -135,7 +135,7 @@ let define_pure_evar_as_lambda env evd evk = let evd1,(na,dom,rng) = match kind_of_term typ with | Prod (na,dom,rng) -> (evd,(na,dom,rng)) | Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd typ - | _ -> error_not_product_loc Loc.ghost env evd typ in + | _ -> error_not_product env evd typ in let avoid = ids_of_named_context (evar_context evi) in let id = next_name_away_with_default_using_types "x" na avoid (Reductionops.whd_evar evd dom) in @@ -191,7 +191,7 @@ let split_tycon loc env evd tycon = | App (c,args) when isEvar c -> let (evd',lam) = define_evar_as_lambda env evd (destEvar c) in real_split evd' (mkApp (lam,args)) - | _ -> error_not_product_loc loc env evd c + | _ -> error_not_product ~loc env evd c in match tycon with | None -> evd,(Anonymous,None,None) |