diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-01 19:45:01 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-02-15 13:12:13 +0100 |
| commit | 968dfdb15cc11d48783017b2a91147b25c854ad6 (patch) | |
| tree | d619d1ebe51d29e5517c9c0385dc4aefe546edbe /pretyping/tacred.ml | |
| parent | 97e1fccd878190a1fc51a1da45f4c06369c0e3db (diff) | |
Monotonizing the Evarutil module.
Some functions were left in the old paradigm because they are only used by the
unification algorithms, so they are not worthwhile to change for now.
Diffstat (limited to 'pretyping/tacred.ml')
| -rw-r--r-- | pretyping/tacred.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index bd46911c9..085aaf78a 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -23,6 +23,7 @@ open Reductionops open Cbv open Patternops open Locus +open Sigma.Notations (* Errors *) @@ -385,7 +386,9 @@ let substl_with_function subst sigma constr = if i <= k + Array.length v then match v.(i-k-1) with | (fx, Some (min, ref)) -> - let (sigma, evk) = Evarutil.new_pure_evar venv !evd dummy in + let sigma = Sigma.Unsafe.of_evar_map !evd in + let Sigma (evk, sigma, _) = Evarutil.new_pure_evar venv sigma dummy in + let sigma = Sigma.to_evar_map sigma in evd := sigma; minargs := Evar.Map.add evk min !minargs; lift k (mkEvar (evk, [|fx;ref|])) |