diff options
| -rw-r--r-- | kernel/environ.ml | 11 | ||||
| -rw-r--r-- | kernel/environ.mli | 5 | ||||
| -rw-r--r-- | tactics/refine.ml | 2 |
3 files changed, 16 insertions, 2 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index ac813e233e..db187880ff 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -131,6 +131,17 @@ let push_rec_types (lna,typarray,_) env = Array.fold_left (fun e assum -> push_rel_assum assum e) env ctxt +let push_named_rec_types (lna,typarray,_) env = + let ctxt = + array_map2_i + (fun i na t -> + match na with + | Name id -> (id, type_app (lift i) t) + | Anonymous -> anomaly "Fix declarations must be named") + lna typarray in + Array.fold_left + (fun e assum -> push_named_assum assum e) env ctxt + let reset_rel_context env = { env with env_context = { env_named_context = env.env_context.env_named_context; diff --git a/kernel/environ.mli b/kernel/environ.mli index adbbf0c5ce..ca93b84e78 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -54,9 +54,12 @@ val names_of_rel_context : env -> names_context (*s Returns also the substitution to be applied to rel's *) val push_rel_context_to_named_context : env -> constr list * env -(*s Push the types of a (co-)fixpoint *) +(*s Push the types of a (co-)fixpoint to [rel_context] *) val push_rec_types : rec_declaration -> env -> env +(*s Push the types of a (co-)fixpoint to [named_context] *) +val push_named_rec_types : rec_declaration -> env -> env + (* Gives identifiers in [named_context] and [rel_context] *) val ids_of_context : env -> identifier list val map_context : (constr -> constr) -> env -> env diff --git a/tactics/refine.ml b/tactics/refine.ml index 1de41c4894..b064f33662 100644 --- a/tactics/refine.ml +++ b/tactics/refine.ml @@ -191,7 +191,7 @@ let rec compute_metamap env c = match kind_of_term c with (* TODO: use a fold *) let vi = Array.map (fresh env) fi in let fi' = Array.map (fun id -> Name id) vi in - let env' = push_rec_types (fi',ai,v) env in + let env' = push_named_rec_types (fi',ai,v) env in let a = Array.map (compute_metamap env') (Array.map (substl (List.map mkVar (Array.to_list vi))) v) |