diff options
| author | Emilio Jesus Gallego Arias | 2018-09-27 22:04:28 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-03 13:52:04 +0200 |
| commit | e11068aa90f6e7fc728d4583998cd99cfa850211 (patch) | |
| tree | 98998fecef98931fea26e5de7d2156c4a6711d42 /pretyping/cases.ml | |
| parent | f19d24a462d50c701a3882de2c16180bb739e622 (diff) | |
[pretyper] Remove imperative passing of evar_map.
Diffstat (limited to 'pretyping/cases.ml')
| -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 37dd3708b3..2c821c96ba 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -408,7 +408,7 @@ let coerce_to_indtype typing_fun env sigma matx tomatchl = (* Utils *) let mkExistential ?(src=(Loc.tag Evar_kinds.InternalHole)) env sigma = - let sigma, (e, u) = new_type_evar env sigma ~src:src univ_flexible_alg in + let sigma, (e, u) = Evarutil.new_type_evar env sigma ~src:src univ_flexible_alg in sigma, e let adjust_tomatch_to_pattern sigma pb ((current,typ),deps,dep) = @@ -1748,7 +1748,7 @@ let build_tycon ?loc env tycon_env s subst tycon extenv sigma t = let n = Context.Rel.length (rel_context !!env) in let n' = Context.Rel.length (rel_context !!tycon_env) in let sigma, (impossible_case_type, u) = - new_type_evar (reset_context !!env) ~src:(Loc.tag ?loc Evar_kinds.ImpossibleCase) + Evarutil.new_type_evar (reset_context !!env) ~src:(Loc.tag ?loc Evar_kinds.ImpossibleCase) sigma univ_flexible_alg in (sigma, lift (n'-n) impossible_case_type, mkSort u) @@ -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, _) = new_type_evar !!env sigma univ_flexible_alg ~src in + let sigma, (t, _) = Evarutil.new_type_evar !!env sigma univ_flexible_alg ~src in sigma, t in (* First strategy: we build an "inversion" predicate, also replacing the *) (* dependencies with existential variables *) |