diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/ide_slave.ml | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 01e37c7c18..36d676f5d9 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -195,10 +195,7 @@ let process_goal sigma g = in let process_hyp d (env,l) = let d = Context.NamedList.Declaration.map_constr (Reductionops.nf_evar sigma) d in - let d' = List.map (fun name -> match pi2 d with - | None -> NamedDecl.LocalAssum (name, pi3 d) - | Some value -> NamedDecl.LocalDef (name, value, pi3 d)) - (pi1 d) in + let d' = Context.NamedList.Declaration.to_named_context d in (List.fold_right Environ.push_named d' env, (Richpp.richpp_of_pp (pr_var_list_decl env sigma d)) :: l) in let (_env, hyps) = |