diff options
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml4 | 2 | ||||
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.mli | 2 | ||||
| -rw-r--r-- | pretyping/evarconv.ml | 8 | ||||
| -rw-r--r-- | pretyping/evarconv.mli | 3 | ||||
| -rw-r--r-- | pretyping/evarsolve.ml | 6 | ||||
| -rw-r--r-- | pretyping/evarsolve.mli | 3 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 2 | ||||
| -rw-r--r-- | pretyping/unification.ml | 6 | ||||
| -rw-r--r-- | proofs/refine.ml | 2 | ||||
| -rw-r--r-- | tactics/class_tactics.ml | 2 | ||||
| -rw-r--r-- | tactics/equality.ml | 3 | ||||
| -rw-r--r-- | toplevel/command.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
13 files changed, 27 insertions, 16 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index a34fa4cae7..88f028b4b7 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -355,7 +355,7 @@ let nf_open_term sigma0 ise c = !s', Evd.evar_universe_context s, c' let unif_end env sigma0 ise0 pt ok = - let ise = Evarconv.consider_remaining_unif_problems env ise0 in + let ise = Evarconv.solve_unif_constraints_with_heuristics env ise0 in let s, uc, t = nf_open_term sigma0 ise pt in let ise1 = create_evar_defs s in let ise1 = Evd.set_universe_context ise1 uc in diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index 74a603e51c..288a04e60a 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -213,7 +213,7 @@ val assert_done : 'a option ref -> 'a (** Very low level APIs. these are calls to evarconv's [the_conv_x] followed by - [consider_remaining_unif_problems] and [resolve_typeclasses]. + [solve_unif_constraints_with_heuristics] and [resolve_typeclasses]. In case of failure they raise [NoMatch] *) val unify_HO : env -> evar_map -> constr -> constr -> evar_map diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 3680cd777a..07f6d9d383 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1081,7 +1081,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = match evar_conv_x ts env_evar evd CUMUL idty evty with | UnifFailure _ -> error "Cannot find an instance" | Success evd -> - match reconsider_conv_pbs (evar_conv_x ts) evd with + match reconsider_unif_constraints (evar_conv_x ts) evd with | UnifFailure _ -> error "Cannot find an instance" | Success evd -> evd @@ -1208,7 +1208,7 @@ let rec solve_unconstrained_evars_with_candidates ts evd = let conv_algo = evar_conv_x ts in let evd = check_evar_instance evd evk a conv_algo in let evd = Evd.define evk a evd in - match reconsider_conv_pbs conv_algo evd with + match reconsider_unif_constraints conv_algo evd with | Success evd -> solve_unconstrained_evars_with_candidates ts evd | UnifFailure _ -> aux l with @@ -1231,7 +1231,7 @@ let solve_unconstrained_impossible_cases env evd = Evd.define evk ty evd' | _ -> evd') evd evd -let consider_remaining_unif_problems env +let solve_unif_constraints_with_heuristics env ?(ts=Conv_oracle.get_transp_state (Environ.oracle env)) evd = let evd = solve_unconstrained_evars_with_candidates ts evd in let rec aux evd pbs progress stuck = @@ -1263,6 +1263,8 @@ let consider_remaining_unif_problems env check_problems_are_solved env heuristic_solved_evd; solve_unconstrained_impossible_cases env heuristic_solved_evd +let consider_remaining_unif_problems = solve_unif_constraints_with_heuristics + (* Main entry points *) exception UnableToUnify of evar_map * unification_error diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 14947c8927..2231e5bc30 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -33,7 +33,10 @@ val e_cumul : env -> ?ts:transparent_state -> evar_map ref -> constr -> constr - (** Try heuristics to solve pending unification problems and to solve evars with candidates *) +val solve_unif_constraints_with_heuristics : env -> ?ts:transparent_state -> evar_map -> evar_map + val consider_remaining_unif_problems : env -> ?ts:transparent_state -> evar_map -> evar_map +(** @deprecated Alias for [solve_unif_constraints_with_heuristics] *) (** Check all pending unification problems are solved and raise an error otherwise *) diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index f1526faccc..f0aa9b564f 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1603,7 +1603,7 @@ let status_changed lev (pbty,_,t1,t2) = (try Evar.Set.mem (head_evar t1) lev with NoHeadEvar -> false) || (try Evar.Set.mem (head_evar t2) lev with NoHeadEvar -> false) -let reconsider_conv_pbs conv_algo evd = +let reconsider_unif_constraints conv_algo evd = let (evd,pbs) = extract_changed_conv_pbs evd status_changed in List.fold_left (fun p (pbty,env,t1,t2 as x) -> @@ -1616,6 +1616,8 @@ let reconsider_conv_pbs conv_algo evd = (Success evd) pbs +let reconsider_conv_pbs = reconsider_unif_constraints + (* Tries to solve problem t1 = t2. * Precondition: t1 is an uninstantiated evar * Returns an optional list of evars that were instantiated, or None @@ -1626,7 +1628,7 @@ let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1) try let t2 = whd_betaiota evd t2 in (* includes whd_evar *) let evd = evar_define conv_algo ~choose env evd pbty ev1 t2 in - reconsider_conv_pbs conv_algo evd + reconsider_unif_constraints conv_algo evd with | NotInvertibleUsingOurAlgorithm t -> UnifFailure (evd,NotClean (ev1,env,t)) diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index f94c83b6dc..b6bdc07889 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -54,7 +54,10 @@ val solve_evar_evar : ?force:bool -> val solve_simple_eqn : conv_fun -> ?choose:bool -> env -> evar_map -> bool option * existential * constr -> unification_result +val reconsider_unif_constraints : conv_fun -> evar_map -> unification_result + val reconsider_conv_pbs : conv_fun -> evar_map -> unification_result +(** @deprecated Alias for [reconsider_unif_constraints] *) val is_unification_pattern_evar : env -> evar_map -> existential -> constr list -> constr -> constr list option diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 6afa55862f..95d854323a 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -290,7 +290,7 @@ let apply_inference_hook hook evdref pending = let apply_heuristics env evdref fail_evar = (* Resolve eagerly, potentially making wrong choices *) - try evdref := consider_remaining_unif_problems + try evdref := solve_unif_constraints_with_heuristics ~ts:(Typeclasses.classes_transparent_state ()) env !evdref with e when CErrors.noncritical e -> let e = CErrors.push e in if fail_evar then iraise e diff --git a/pretyping/unification.ml b/pretyping/unification.ml index fc63015a8e..259318693f 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1220,7 +1220,7 @@ let is_mimick_head ts f = let try_to_coerce env evd c cty tycon = let j = make_judge c cty in let (evd',j') = inh_conv_coerce_rigid_to true Loc.ghost env evd j tycon in - let evd' = Evarconv.consider_remaining_unif_problems env evd' in + let evd' = Evarconv.solve_unif_constraints_with_heuristics env evd' in let evd' = Evd.map_metas_fvalue (nf_evar evd') evd' in (evd',j'.uj_val) @@ -1272,8 +1272,8 @@ let solve_simple_evar_eqn ts env evd ev rhs = | Success evd -> if Flags.version_less_or_equal Flags.V8_5 then (* We used to force solving unrelated problems at arbitrary times *) - Evarconv.consider_remaining_unif_problems env evd - else (* solve_simple_eqn calls reconsider_conv_pbs itself *) + Evarconv.solve_unif_constraints_with_heuristics env evd + else (* solve_simple_eqn calls reconsider_unif_constraints itself *) evd (* [w_merge env sigma b metas evars] merges common instances in metas diff --git a/proofs/refine.ml b/proofs/refine.ml index 2f21428900..3f55270609 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -157,6 +157,6 @@ end } let solve_constraints = let open Proofview in tclENV >>= fun env -> tclEVARMAP >>= fun sigma -> - try let sigma = Evarconv.consider_remaining_unif_problems env sigma in + try let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in Unsafe.tclEVARSADVANCE sigma with e -> tclZERO e diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 0944cbe38f..9ea4027263 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1437,7 +1437,7 @@ let initial_select_evars filter = let resolve_typeclass_evars debug depth unique env evd filter split fail = let evd = - try Evarconv.consider_remaining_unif_problems + try Evarconv.solve_unif_constraints_with_heuristics ~ts:(Typeclasses.classes_transparent_state ()) env evd with e when CErrors.noncritical e -> evd in diff --git a/tactics/equality.ml b/tactics/equality.ml index e9d08d7375..bb3cbad92b 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1163,7 +1163,8 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = let dflt_typ = unsafe_type_of env sigma dflt in try let () = evdref := Evarconv.the_conv_x_leq env dflt_typ p_i !evdref in - let () = evdref := Evarconv.consider_remaining_unif_problems env !evdref in + let () = + evdref := Evarconv.solve_unif_constraints_with_heuristics env !evdref in dflt with Evarconv.UnableToUnify _ -> error "Cannot solve a unification problem." diff --git a/toplevel/command.ml b/toplevel/command.ml index 12c387dcf3..7ffe680e5e 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -1129,7 +1129,7 @@ let interp_recursive isfix fixl notations = () in (* Instantiate evars and check all are resolved *) - let evd = consider_remaining_unif_problems env_rec !evdref in + let evd = solve_unif_constraints_with_heuristics env_rec !evdref in let evd, nf = nf_evars_and_universes evd in let fixdefs = List.map (Option.map nf) fixdefs in let fixtypes = List.map nf fixtypes in diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index f69bac437e..9d3837d2e2 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1497,7 +1497,7 @@ let get_current_context_of_args = function let vernac_check_may_eval redexp glopt rc = let (sigma, env) = get_current_context_of_args glopt in let sigma', c = interp_open_constr env sigma rc in - let sigma' = Evarconv.consider_remaining_unif_problems env sigma' in + let sigma' = Evarconv.solve_unif_constraints_with_heuristics env sigma' in Evarconv.check_problems_are_solved env sigma'; let sigma',nf = Evarutil.nf_evars_and_universes sigma' in let pl, uctx = Evd.universe_context sigma' in |