diff options
| author | Pierre-Marie Pédrot | 2018-11-27 11:16:20 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-27 11:16:20 +0100 |
| commit | dddb72b2f45f39f04e91aa9099bcd1064c629504 (patch) | |
| tree | c40abe89eb032919ddb84c657adf173a05a46f51 | |
| parent | e828ffaf1df8deb250ade91123b20b4d53c88060 (diff) | |
| parent | 7681a634ac7396e0e714323054d7cc55f106d8df (diff) | |
Merge PR #7696: Remove some univ_flexible_alg from cases
| -rw-r--r-- | pretyping/cases.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index e02fb33276..fe67f5767b 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -995,7 +995,7 @@ let expand_arg tms (p,ccl) ((_,t),_,na) = let use_unit_judge env evd = let j, ctx = coq_unit_judge !!env in - let evd' = Evd.merge_context_set Evd.univ_flexible_alg evd ctx in + let evd' = Evd.merge_context_set Evd.univ_flexible evd ctx in evd', j let add_assert_false_case pb tomatch = @@ -2037,7 +2037,7 @@ let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred = | None -> (* No type constraint: we first create a generic evar type constraint *) let src = (loc, Evar_kinds.CasesType false) in - let sigma, (t, _) = Evarutil.new_type_evar !!env sigma univ_flexible_alg ~src in + let sigma, (t, _) = Evarutil.new_type_evar !!env sigma univ_flexible ~src in sigma, t in (* First strategy: we build an "inversion" predicate, also replacing the *) (* dependencies with existential variables *) @@ -2061,7 +2061,7 @@ let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred = | Some rtntyp -> (* We extract the signature of the arity *) let building_arsign,envar = List.fold_right_map (push_rel_context sigma) arsign env in - let sigma, newt = new_sort_variable univ_flexible_alg sigma in + let sigma, newt = new_sort_variable univ_flexible sigma in let sigma, predcclj = typing_fun (mk_tycon (mkSort newt)) envar sigma rtntyp in let predccl = nf_evar sigma predcclj.uj_val in [sigma, predccl, building_arsign] |