diff options
| author | Matthieu Sozeau | 2018-08-15 14:22:15 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2019-02-08 11:14:10 +0100 |
| commit | 2cf15ef8e3ddebe285ec0e9f5f8715b025ba4eec (patch) | |
| tree | 4d4e075161b3d54e7fd49ed90d830f2e478aac6e /pretyping/evarconv.ml | |
| parent | af9b88c253b578ad53ee884ff3102d0a74056a1e (diff) | |
Rename types_or_terms and the unification function types
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 25 |
1 files changed, 20 insertions, 5 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 0e69dd43d5..8f7c88b0db 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -424,7 +424,10 @@ let conv_fun f flags on_types = in let termfn env evd pbty term1 term2 = f flags env evd pbty term1 term2 - in if on_types then typefn else termfn + in + match on_types with + | TypeUnification -> typefn + | TermUnification -> termfn let rec evar_conv_x flags env evd pbty term1 term2 = let term1 = whd_head_evar evd term1 in @@ -735,7 +738,11 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty match ise_stack2 false env i (evar_conv_x flags) sk1 sk2 with |None, Success i' -> Success (solve_refl flags (fun p env i pbty a1 a2 -> - let flags = if p then default_flags env else flags in + let flags = + match p with + | TypeUnification -> default_flags env + | TermUnification -> flags + in is_success (evar_conv_x flags env i pbty a1 a2)) env i' (position_problem true pbty) sp1 al1 al2) |_, (UnifFailure _ as x) -> x @@ -967,7 +974,11 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty |None, Success i' -> (** FIXME: solve_refl can restrict the evar, do we want to allow that? *) Success (solve_refl flags (fun p env i pbty a1 a2 -> - let flags = if p then default_flags env else flags in + let flags = + match p with + | TypeUnification -> default_flags env + | TermUnification -> flags + in is_success (evar_conv_x flags env i pbty a1 a2)) env i' (position_problem true pbty) sp1 al1 al2) |_, (UnifFailure _ as x) -> x @@ -1544,8 +1555,12 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 = UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason))) | Evar (evk1,args1), Evar (evk2,args2) when Evar.equal evk1 evk2 -> let f ontype env evd pbty x y = - let reds = if ontype then full_transparent_state else flags.open_ts in - is_fconv ~reds pbty env evd x y in + let reds = + match ontype with + | TypeUnification -> full_transparent_state + | TermUnification -> flags.open_ts + in is_fconv ~reds pbty env evd x y + in Success (solve_refl ~can_drop:true flags f env evd (position_problem true pbty) evk1 args1 args2) | Evar ev1, Evar ev2 when app_empty -> |