From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 7 Nov 2005 18:46:56 +0000 (+0000)
Subject: Let-ins with types can now be produced.
X-Git-Tag: V_0_7_2_3~112
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=99171b0e4bd02486bd99208bbca911eba03c7af7;p=helm.git

Let-ins with types can now be produced.
---

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