From 99171b0e4bd02486bd99208bbca911eba03c7af7 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 7 Nov 2005 18:46:56 +0000 Subject: [PATCH] Let-ins with types can now be produced. --- helm/ocaml/tactics/primitiveTactics.ml | 7 ++++++- helm/ocaml/tactics/proofEngineHelpers.ml | 10 ++++++---- 2 files changed, 12 insertions(+), 5 deletions(-) diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml index 96ff130c5..ca6b0e582 100644 --- a/helm/ocaml/tactics/primitiveTactics.ml +++ b/helm/ocaml/tactics/primitiveTactics.ml @@ -152,7 +152,12 @@ let classify_metas newmeta in_subst_domain subst_in metasenv = | Some (n,Cic.Def (s,None)) -> Some (n,Cic.Def ((subst_in canonical_context' s),None)) | None -> None - | Some (_,Cic.Def (_,Some _)) -> assert false + | Some (n,Cic.Def (bo,Some ty)) -> + Some + (n, + Cic.Def + (subst_in canonical_context' bo, + Some (subst_in canonical_context' ty))) in entry'::canonical_context' ) canonical_context [] diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml index 9f7fb42f4..fd336910e 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.ml +++ b/helm/ocaml/tactics/proofEngineHelpers.ml @@ -46,9 +46,10 @@ let subst_meta_in_proof proof meta term newmetasenv = List.map (function Some (n,Cic.Decl s) -> Some (n,Cic.Decl (subst_in s)) - | Some (n,Cic.Def (s,None)) -> Some (n,Cic.Def ((subst_in s),None)) + | Some (n,Cic.Def (s,None)) -> Some (n,Cic.Def (subst_in s,None)) | None -> None - | Some (_,Cic.Def (_,Some _)) -> assert false + | Some (n,Cic.Def (bo,Some ty)) -> + Some (n,Cic.Def (subst_in bo,Some (subst_in ty))) ) canonical_context in i,canonical_context',(subst_in ty) @@ -92,8 +93,9 @@ let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv = None -> None | Some (i,Cic.Decl t) -> Some (i,Cic.Decl (subst_in t)) | Some (i,Cic.Def (t,None)) -> - Some (i,Cic.Def ((subst_in t),None)) - | Some (_,Cic.Def (_,Some _)) -> assert false + Some (i,Cic.Def (subst_in t,None)) + | Some (i,Cic.Def (bo,Some ty)) -> + Some (i,Cic.Def (subst_in bo,Some (subst_in ty))) ) canonical_context in (m,canonical_context',subst_in ty)::i -- 2.39.2