diff options
| author | Maxime Dénès | 2017-06-06 17:18:59 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-06 17:18:59 +0200 |
| commit | e5581b2a1e5b3d9fc5dc7fe95ee4ba121f5d42cd (patch) | |
| tree | 1a0d0b7d693c37ca8712057e946587584687208e /pretyping/cases.ml | |
| parent | 2f23c27e08f66402b8fba4745681becd402f4c5c (diff) | |
| parent | 0ce9cef0ac431e184c870617841bedc3f427396d (diff) | |
Merge PR#623: Remove the Sigma (monotonous state) API.
Diffstat (limited to 'pretyping/cases.ml')
| -rw-r--r-- | pretyping/cases.ml | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index efab5b9779..c3f392980a 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -32,7 +32,6 @@ open Evardefine open Evarsolve open Evarconv open Evd -open Sigma.Notations open Context.Rel.Declaration module RelDecl = Context.Rel.Declaration @@ -2000,10 +1999,8 @@ let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred = let sigma,t = match tycon with | Some t -> refresh_tycon sigma t | None -> - let sigma = Sigma.Unsafe.of_evar_map sigma in - let Sigma ((t, _), sigma, _) = + let (sigma, (t, _)) = new_type_evar env sigma univ_flexible_alg ~src:(Loc.tag ?loc @@ Evar_kinds.CasesType false) in - let sigma = Sigma.to_evar_map sigma in sigma, t in (* First strategy: we build an "inversion" predicate *) |