X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FproofEngineHelpers.ml;h=79304211deb0e8a69f3f1072a8657dc2a33510fa;hb=0de1b960f42ac368414b7405a79e7933445ee8af;hp=16be77edb443c84c3c7845182564dacfb1601cce;hpb=bac72fcaa876137ab7a5630e0c1badc2a627dce8;p=helm.git diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml index 16be77edb..79304211d 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.ml +++ b/helm/ocaml/tactics/proofEngineHelpers.ml @@ -36,6 +36,7 @@ let mk_fresh_name context name ~typ = (try (match CicTypeChecker.type_of_aux' [] context typ with C.Sort C.Prop -> "H" + | C.Sort C.CProp -> "H" | C.Sort C.Set -> "x" | _ -> "H" ) @@ -100,8 +101,9 @@ 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) -> Some (n,Cic.Def (subst_in s)) + | Some (n,Cic.Def (s,None)) -> Some (n,Cic.Def ((subst_in s),None)) | None -> None + | Some (_,Cic.Def (_,Some _)) -> assert false ) canonical_context in i,canonical_context',(subst_in ty) @@ -136,7 +138,9 @@ let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv = (function None -> None | Some (i,Cic.Decl t) -> Some (i,Cic.Decl (subst_in t)) - | Some (i,Cic.Def t) -> Some (i,Cic.Def (subst_in t)) + | Some (i,Cic.Def (t,None)) -> + Some (i,Cic.Def ((subst_in t),None)) + | Some (_,Cic.Def (_,Some _)) -> assert false ) canonical_context in (m,canonical_context',subst_in ty)::i