From 0438f9389664c29ece1045ad3e6657d6756a1fd8 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 20 Oct 2006 14:35:22 +0000 Subject: [PATCH] New function pack_coercion_metasenv, used in auto after try_candidates to clean up the metasenv (othewise application could fail). --- components/cic_unification/cicRefine.ml | 49 +++++++++++++----------- components/cic_unification/cicRefine.mli | 1 + 2 files changed, 27 insertions(+), 23 deletions(-) diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml index 0a6510b44..dee8ba5f3 100644 --- a/components/cic_unification/cicRefine.ml +++ b/components/cic_unification/cicRefine.ml @@ -1809,6 +1809,31 @@ let pack_coercion metasenv ctx t = merge_coercions ctx t ;; +let pack_coercion_metasenv conjectures = + let module C = Cic in + List.map + (fun (i, ctx, ty) -> + let ctx = + List.fold_right + (fun item ctx -> + let item' = + match item with + Some (name, C.Decl t) -> + Some (name, C.Decl (pack_coercion conjectures ctx t)) + | Some (name, C.Def (t,None)) -> + Some (name,C.Def (pack_coercion conjectures ctx t,None)) + | Some (name, C.Def (t,Some ty)) -> + Some (name, C.Def (pack_coercion conjectures ctx t, + Some (pack_coercion conjectures ctx ty))) + | None -> None + in + item'::ctx + ) ctx [] + in + ((i,ctx,pack_coercion conjectures ctx ty)) + ) conjectures +;; + let pack_coercion_obj obj = let module C = Cic in match obj with @@ -1829,29 +1854,7 @@ let pack_coercion_obj obj = let ty = pack_coercion [] [] ty in C.Variable (name, body, ty, params, attrs) | C.CurrentProof (name, conjectures, body, ty, params, attrs) -> - let conjectures = - List.map - (fun (i, ctx, ty) -> - let ctx = - List.fold_right - (fun item ctx -> - let item' = - match item with - Some (name, C.Decl t) -> - Some (name, C.Decl (pack_coercion conjectures ctx t)) - | Some (name, C.Def (t,None)) -> - Some (name,C.Def (pack_coercion conjectures ctx t,None)) - | Some (name, C.Def (t,Some ty)) -> - Some (name, C.Def (pack_coercion conjectures ctx t, - Some (pack_coercion conjectures ctx ty))) - | None -> None - in - item'::ctx - ) ctx [] - in - ((i,ctx,pack_coercion conjectures ctx ty)) - ) conjectures - in + let conjectures = pack_coercion_metasenv conjectures in let body = pack_coercion conjectures [] body in let ty = pack_coercion conjectures [] ty in C.CurrentProof (name, conjectures, body, ty, params, attrs) diff --git a/components/cic_unification/cicRefine.mli b/components/cic_unification/cicRefine.mli index be1069e71..30b264455 100644 --- a/components/cic_unification/cicRefine.mli +++ b/components/cic_unification/cicRefine.mli @@ -48,3 +48,4 @@ val insert_coercions: bool ref (* initially true *) val pack_coercion_obj: Cic.obj -> Cic.obj +val pack_coercion_metasenv: Cic.metasenv -> Cic.metasenv -- 2.39.2