X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FprimitiveTactics.ml;h=8dfdd66c494cb2659ce11294dfeb4490928d8442;hb=265cf771fbfe217b5f274b999fc3ad887683a09a;hp=91cd6198ef8bb28d6d60f7a42a8450fdfa62bcc8;hpb=edf601b6b8eb5b28a5292d0660a3b54b5680e580;p=helm.git

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 91cd6198e..8dfdd66c4 100644
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -50,7 +50,7 @@ let lambda_abstract context newmeta ty mk_fresh_name =
          (context',ty,C.Lambda(n',s,bo))
     | C.LetIn (n,s,t) ->
        let (context',ty,bo) =
-        collect_context ((Some (n,(C.Def s)))::context) t
+        collect_context ((Some (n,(C.Def (s,None))))::context) t
        in
         (context',ty,C.LetIn(n,s,bo))
     | _ as t ->
@@ -132,9 +132,10 @@ let classify_metas newmeta in_subst_domain subst_in metasenv =
            match entry with
               Some (n,Cic.Decl s) ->
                Some (n,Cic.Decl (subst_in canonical_context' s))
-            | Some (n,Cic.Def s) ->
-               Some (n,Cic.Def (subst_in canonical_context' s))
+            | Some (n,Cic.Def (s,None)) ->
+               Some (n,Cic.Def ((subst_in canonical_context' s),None))
             | None -> None
+            | Some (_,Cic.Def (_,Some _)) -> assert false
           in
            entry'::canonical_context'
         ) canonical_context []
@@ -361,7 +362,7 @@ let letin_tac
     let fresh_name =
      mk_fresh_name_callback context (Cic.Name "Hletin") ~typ:term in
     let context_for_newmeta =
-     (Some (fresh_name,C.Def term))::context in
+     (Some (fresh_name,C.Def (term,None)))::context in
     let irl =
      identity_relocation_list_for_metavariable context_for_newmeta in
      let newmetaty = CicSubstitution.lift 1 ty in
@@ -547,9 +548,10 @@ let change_tac ~what ~with_what ~status:(proof, goal) =
     let context' =
      List.map
       (function
-          Some (name,Cic.Def  t) -> Some (name,Cic.Def  (replace t))
+          Some (name,Cic.Def (t,None)) -> Some (name,Cic.Def ((replace t),None))
         | Some (name,Cic.Decl t) -> Some (name,Cic.Decl (replace t))
         | None -> None
+        | Some (_,Cic.Def (_,Some _)) -> assert false
       ) context
     in
      let metasenv' =