old subst tactics removed. New destruct tactic used instead

[helm.git] / matita / contribs / LOGIC / datatypes / Context.ma

diff --git a/matita/contribs/LOGIC/datatypes/Context.ma b/matita/contribs/LOGIC/datatypes/Context.ma
index 0de237801b71b229337df9761ccd871b5dd1896a..44d62664850afe025d1be429465e980515a36781 100644 (file)
--- a/matita/contribs/LOGIC/datatypes/Context.ma
+++ b/matita/contribs/LOGIC/datatypes/Context.ma
@@ -19,13 +19,15 @@ set "baseuri" "cic:/matita/LOGIC/datatypes/Context".
      - contexts: P Q
 *)
 
+include "datatypes/Proof.ma".
 include "datatypes/Sequent.ma".
 
 inductive Context: Type \def
    | leaf: Context
-   | abst: Context \to Sequent \to Context
+   | abst: Context \to Proof \to Proof \to Sequent \to Context
 .
-
+(*
 definition inj: Sequent \to Context \def abst leaf.
 
 coercion cic:/matita/LOGIC/datatypes/Context/inj.con.
+*)