diff options
| author | Enrico Tassi | 2018-11-09 14:04:17 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2018-11-14 10:49:59 +0100 |
| commit | 3b73e80593c9508a880c7d6e442abb8c82523a36 (patch) | |
| tree | 0d2c8b5523c3b3345f06e1869bde4cfe6146aab3 /plugins | |
| parent | 94494770254bec236f2f6fe727ae42b79192afe4 (diff) | |
ssrmatching: unify_HO does not resolve type classes
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml | 8 | ||||
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.mli | 2 |
2 files changed, 6 insertions, 4 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index bb6decd848..5dcbf9b3ef 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -354,14 +354,16 @@ let nf_open_term sigma0 ise c = let c' = nf c in let _ = Evd.fold copy_def sigma0 () in !s', Evd.evar_universe_context s, EConstr.of_constr c' -let unif_end env sigma0 ise0 pt ok = +let unif_end ?(solve_TC=true) env sigma0 ise0 pt ok = let ise = Evarconv.solve_unif_constraints_with_heuristics env ise0 in let tcs = Evd.get_typeclass_evars ise in let s, uc, t = nf_open_term sigma0 ise pt in let ise1 = create_evar_defs s in let ise1 = Evd.set_typeclass_evars ise1 (Evar.Set.filter (fun ev -> Evd.is_undefined ise1 ev) tcs) in let ise1 = Evd.set_universe_context ise1 uc in - let ise2 = Typeclasses.resolve_typeclasses ~fail:true env ise1 in + let ise2 = + if solve_TC then Typeclasses.resolve_typeclasses ~fail:true env ise1 + else ise1 in if not (ok ise) then raise NoProgress else if ise2 == ise1 then (s, uc, t) else @@ -370,7 +372,7 @@ let unif_end env sigma0 ise0 pt ok = let unify_HO env sigma0 t1 t2 = let sigma = unif_HO env sigma0 t1 t2 in - let sigma, uc, _ = unif_end env sigma0 sigma t2 (fun _ -> true) in + let sigma, uc, _ = unif_end ~solve_TC:false env sigma0 sigma t2 (fun _ -> true) in Evd.set_universe_context sigma uc let pf_unify_HO gl t1 t2 = diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index f478d48ea3..b3ddb52e85 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -201,7 +201,7 @@ val assert_done : 'a option ref -> 'a (** Very low level APIs. these are calls to evarconv's [the_conv_x] followed by - [solve_unif_constraints_with_heuristics] and [resolve_typeclasses]. + [solve_unif_constraints_with_heuristics]. In case of failure they raise [NoMatch] *) val unify_HO : env -> evar_map -> EConstr.constr -> EConstr.constr -> evar_map |