diff options
| author |  Matej Kosik <matej.kosik@inria.fr> | 2016-08-15 14:14:14 +0200 |
|---|---|---|
| committer |  Matej Kosik <m4tej.kosik@gmail.com> | 2016-08-25 10:52:44 +0200 |
| commit | 1297523bffdc3a9fe3e447acc6837be835e86d06 (patch) | |
| tree | 04b0db664081d14add21fe3a9934d609d8b749f0 /ide | |
| parent | 3e6bc0e8d09e3eb913b366b4f5db280154b94018 (diff) | |
CLEANUP: changing the definition of the "Context.NamedList.Declaration" type
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 01e37c7c1..36d676f5d 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) = |