diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/indfun.ml | 3 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 10 |
2 files changed, 8 insertions, 5 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 0cacb003d8..1c5eb16218 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -132,6 +132,7 @@ let rec abstract_glob_constr c = function | Constrexpr.LocalRawAssum (idl,k,t)::bl -> List.fold_right (fun x b -> Constrexpr_ops.mkLambdaC([x],k,t,b)) idl (abstract_glob_constr c bl) + | Constrexpr.LocalPattern _::bl -> assert false let interp_casted_constr_with_implicits env sigma impls c = Constrintern.intern_gen Pretyping.WithoutTypeConstraint env ~impls @@ -215,6 +216,7 @@ let rec local_binders_length = function | [] -> 0 | Constrexpr.LocalRawDef _::bl -> 1 + local_binders_length bl | Constrexpr.LocalRawAssum (idl,_,_)::bl -> List.length idl + local_binders_length bl + | Constrexpr.LocalPattern _::bl -> assert false let prepare_body ((name,_,args,types,_),_) rt = let n = local_binders_length args in @@ -861,6 +863,7 @@ let make_graph (f_ref:global_reference) = (fun (loc,n) -> CRef(Libnames.Ident(loc, Nameops.out_name n),None)) nal + | Constrexpr.LocalPattern _ -> assert false ) nal_tas ) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 95b4967faa..e742f7b80d 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1516,13 +1516,13 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let functional_id = add_suffix function_name "_F" in let term_id = add_suffix function_name "_terminate" in let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx:(snd (Evd.universe_context evm)) res in + (* Refresh the global universes, now including those of _F *) + let evm = Evd.from_env (Global.env ()) in let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> LocalAssum (x,t)) pre_rec_args) env in - let relation = - fst (*FIXME*)(interp_constr - env_with_pre_rec_args - (Evd.from_env env_with_pre_rec_args) - r) + let relation, evuctx = + interp_constr env_with_pre_rec_args evm r in + let evm = Evd.from_ctx evuctx in let tcc_lemma_name = add_suffix function_name "_tcc" in let tcc_lemma_constr = ref None in (* let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *) |