diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-31 17:43:18 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-13 12:57:39 +0200 |
| commit | 3a0b543af4ac99b29efdebe27b1d204d044a7bf0 (patch) | |
| tree | e1f926647c686a559b045654924a50535afa25c0 /pretyping/tacred.ml | |
| parent | f3b84cf63c242623bdcccd30c536e55983971da5 (diff) | |
Evar maps contain econstrs.
We bootstrap the circular evar_map <-> econstr dependency by moving
the internal EConstr.API module to Evd.MiniEConstr. Then we make the
Evd functions use econstr.
Diffstat (limited to 'pretyping/tacred.ml')
| -rw-r--r-- | pretyping/tacred.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 977713fd8..696001ab7 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -416,7 +416,7 @@ exception Partial reduction is solved by the expanded fix term. *) let solve_arity_problem env sigma fxminargs c = let evm = ref sigma in - let set_fix i = evm := Evd.define i (Constr.mkVar vfx) !evm in + let set_fix i = evm := Evd.define i (mkVar vfx) !evm in let rec check strict c = let c' = whd_betaiotazeta sigma c in let (h,rcargs) = decompose_app_vect sigma c' in @@ -641,7 +641,7 @@ let whd_nothing_for_iota env sigma s = | _ -> s) | Evar ev -> s | Meta ev -> - (try whrec (EConstr.of_constr (Evd.meta_value sigma ev), stack) + (try whrec (Evd.meta_value sigma ev, stack) with Not_found -> s) | Const (const, u) when is_transparent_constant full_transparent_state const -> let u = EInstance.kind sigma u in |