diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-11 23:07:14 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-06-18 14:16:33 +0200 |
| commit | 89a85a6603b7112e685a052d728284d3e4c2881e (patch) | |
| tree | f3a3c51bd32439eeab9c2138d45a115adffa7850 /tactics/tactics.ml | |
| parent | 0daf6af5949dbc7304e9fc3adf063519d5a60c4b (diff) | |
Fix #7421: constr_eq ignores universe constraints.
The test isn't quite the one in #7421 because that use of algebraic
universes is wrong.
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 770e31fea..c430edf2e 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -5034,6 +5034,26 @@ let tclABSTRACT ?(opaque=true) name_op tac = else name_op_to_name name_op (DefinitionBody Definition) "_subterm" in abstract_subproof ~opaque s gk tac +let constr_eq ~strict x y = + let fail = Tacticals.New.tclFAIL 0 (str "Not equal") in + let fail_universes = Tacticals.New.tclFAIL 0 (str "Not equal (due to universes)") in + Proofview.Goal.enter begin fun gl -> + let env = Tacmach.New.pf_env gl in + let evd = Tacmach.New.project gl in + match EConstr.eq_constr_universes env evd x y with + | Some csts -> + let csts = UnivProblem.to_constraints ~force_weak:false (Evd.universes evd) csts in + if strict then + if Evd.check_constraints evd csts then Proofview.tclUNIT () + else fail_universes + else + (match Evd.add_constraints evd csts with + | evd -> Proofview.Unsafe.tclEVARS evd + | exception Univ.UniverseInconsistency _ -> + fail_universes) + | None -> fail + end + let unify ?(state=full_transparent_state) x y = Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in |