Defs in context may now have an optional type (when unknown).

[helm.git] / helm / ocaml / tactics / primitiveTactics.ml

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 91cd6198ef8bb28d6d60f7a42a8450fdfa62bcc8..8dfdd66c494cb2659ce11294dfeb4490928d8442 100644 (file)
--- 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' =