diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 25 |
1 files changed, 17 insertions, 8 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 52179ae508..5548833d6b 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -361,20 +361,29 @@ let add_pat_variables pat typ env : Environ.env = fst ( Context.Rel.fold_outside (fun decl (env,ctxt) -> - let _,v,t = Context.Rel.Declaration.to_tuple decl in - match Context.Rel.Declaration.get_name decl with - | Anonymous -> assert false - | Name id -> + let open Context.Rel.Declaration in + (*let _,v,t = Context.Rel.Declaration.to_tuple decl in*) + match decl with + | LocalAssum (Anonymous,_) | LocalDef (Anonymous,_,_) -> assert false + | LocalAssum (Name id, t) -> let new_t = substl ctxt t in - let new_v = Option.map (substl ctxt) v in + observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++ + str "old type := " ++ Printer.pr_lconstr t ++ fnl () ++ + str "new type := " ++ Printer.pr_lconstr new_t ++ fnl () + ); + let open Context.Named.Declaration in + (Environ.push_named (LocalAssum (id,new_t)) env,mkVar id::ctxt) + | LocalDef (Name id, v, t) -> + let new_t = substl ctxt t in + let new_v = substl ctxt v in observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++ str "old type := " ++ Printer.pr_lconstr t ++ fnl () ++ str "new type := " ++ Printer.pr_lconstr new_t ++ fnl () ++ - Option.fold_right (fun v _ -> str "old value := " ++ Printer.pr_lconstr v ++ fnl ()) v (mt ()) ++ - Option.fold_right (fun v _ -> str "new value := " ++ Printer.pr_lconstr v ++ fnl ()) new_v (mt ()) + str "old value := " ++ Printer.pr_lconstr v ++ fnl () ++ + str "new value := " ++ Printer.pr_lconstr new_v ++ fnl () ); let open Context.Named.Declaration in - (Environ.push_named (of_tuple (id,new_v,new_t)) env,mkVar id::ctxt) + (Environ.push_named (LocalDef (id,new_v,new_t)) env,mkVar id::ctxt) ) (Environ.rel_context new_env) ~init:(env,[]) |