diff options
| author | Maxime Dénès | 2017-08-16 09:44:28 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-08-16 09:44:28 +0200 |
| commit | e1264c9f0d50bf8ca09fa7388101daa0b4c29635 (patch) | |
| tree | 3358d182b655bb2510c1d99872ac733474c9124a /plugins/funind/indfun.ml | |
| parent | 09b54382e52b572f8c091993309adcc4fea3a093 (diff) | |
| parent | cf906af70f5c48cab99bd89047af0b2831850cf1 (diff) | |
Merge PR #912: Detyping functions are now operating on EConstr.t.
Diffstat (limited to 'plugins/funind/indfun.ml')
| -rw-r--r-- | plugins/funind/indfun.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 89537ad3f6..8769f56688 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -618,7 +618,7 @@ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacex let fixl,ntns = Command.extract_fixpoint_components false fixpoint_exprl in let ((_,_,typel),_,ctx,_) = Command.interp_fixpoint fixl ntns in let constr_expr_typel = - with_full_print (List.map (Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx))) typel in + with_full_print (List.map (fun c -> Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx) (EConstr.of_constr c))) typel in let fixpoint_exprl_with_new_bl = List.map2 (fun ((lna,(rec_arg_opt,rec_order),bl,ret_typ,opt_body),notation_list) fix_typ -> @@ -855,9 +855,9 @@ let make_graph (f_ref:global_reference) = let sigma = Evd.from_env env in let extern_body,extern_type = with_full_print (fun () -> - (Constrextern.extern_constr false env sigma body, + (Constrextern.extern_constr false env sigma (EConstr.of_constr body), Constrextern.extern_type false env sigma - ((*FIXME*) c_body.const_type) + (EConstr.of_constr (*FIXME*) c_body.const_type) ) ) () |