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 /plugins/funind/glob_termops.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 'plugins/funind/glob_termops.ml')
| -rw-r--r-- | plugins/funind/glob_termops.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 40ea40b6b..845104c3c 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -564,6 +564,7 @@ let resolve_and_replace_implicits ?(flags=Pretyping.all_and_fail_flags) ?(expect If someone knows how to prevent solved existantial removal in understand, please do not hesitate to change the computation of [ctx] here *) let ctx,_,_ = Pretyping.ise_pretype_gen flags env sigma Glob_ops.empty_lvar expected_type rt in let ctx, f = Evarutil.nf_evars_and_universes ctx in + let f c = EConstr.of_constr (f (EConstr.Unsafe.to_constr c)) in (* then we map [rt] to replace the implicit holes by their values *) let rec change rt = @@ -586,8 +587,8 @@ If someone knows how to prevent solved existantial removal in understand, pleas with Found evi -> (* we found the evar corresponding to this hole *) match evi.evar_body with | Evar_defined c -> - (* we just have to lift the solution in glob_term *) - Detyping.detype Detyping.Now false Id.Set.empty env ctx (EConstr.of_constr (f c)) + (* we just have to lift the solution in glob_term *) + Detyping.detype Detyping.Now false Id.Set.empty env ctx (f c) | Evar_empty -> rt (* the hole was not solved : we do nothing *) ) | (GHole(BinderType na,_,_)) -> (* we only want to deal with implicit arguments *) @@ -609,7 +610,7 @@ If someone knows how to prevent solved existantial removal in understand, pleas match evi.evar_body with | Evar_defined c -> (* we just have to lift the solution in glob_term *) - Detyping.detype Detyping.Now false Id.Set.empty env ctx (EConstr.of_constr (f c)) + Detyping.detype Detyping.Now false Id.Set.empty env ctx (f c) | Evar_empty -> rt (* the hole was not solved : we d when falseo nothing *) in res |