From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 4 Jul 2005 14:09:02 +0000 (+0000)
Subject: New command   default "foo" uri1 ... urin
X-Git-Tag: PRE_GETTER_STORAGE~7
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f94eb70000832bc252cd4a510a1ede4d8197a4a8;p=helm.git

New command   default "foo" uri1 ... urin
to set uri1 ... urin as the default foo.

Actually it can be used to set the current equality, true, false and absurd
like this:

default "equality" equri sym_equri transeq_uri eq_induri eq_ind_ruri.
default "true" trueuri.
default "false" falseuri.
default "absurd" absurduri.
---

diff --git a/helm/matita/library/equality.ma b/helm/matita/library/equality.ma
index d700ddd07..90ce050e3 100644
--- a/helm/matita/library/equality.ma
+++ b/helm/matita/library/equality.ma
@@ -38,6 +38,13 @@ theorem f_equal: \forall  A,B:Type.\forall f:A\to B.
 intros.elim H.reflexivity.
 qed.
 
+default "equality"
+ cic:/matita/equality/eq.ind
+ cic:/matita/equality/sym_eq.con
+ cic:/matita/equality/trans_eq.con
+ cic:/matita/equality/eq_ind.con
+ cic:/matita/equality/eq_ind_r.con. 
+
 theorem f_equal2: \forall  A,B,C:Type.\forall f:A\to B \to C.
 \forall x1,x2:A. \forall y1,y2:B.
 eq A x1 x2\to eq B y1 y2\to eq C (f x1 y1) (f x2 y2).
diff --git a/helm/matita/library/logic.ma b/helm/matita/library/logic.ma
index a509bbb8d..fd3744396 100644
--- a/helm/matita/library/logic.ma
+++ b/helm/matita/library/logic.ma
@@ -18,8 +18,12 @@ set "baseuri" "cic:/matita/logic/".
 inductive True: Prop \def
 I : True.
 
+default "true" cic:/matita/logic/True.ind.
+
 inductive False: Prop \def .
 
+default "false" cic:/matita/logic/False.ind.
+
 definition Not: Prop \to Prop \def
 \lambda A. (A \to False).
 
@@ -27,6 +31,8 @@ theorem absurd : \forall A,C:Prop. A \to Not A \to C.
 intros. elim (H1 H).
 qed.
 
+default "absurd" cic:/matita/logic/absurd.ind.
+
 inductive And (A,B:Prop) : Prop \def
     conj : A \to B \to (And A B).
 
diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index df8f484ba..cb420d267 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -224,6 +224,10 @@ let eval_from_stream_ref = ref (fun _ _ _ -> assert false);;
  
 let eval_command status cmd =
   match cmd with
+  | TacticAst.Default (loc, what, uris) as cmd ->
+     LibraryObjects.set_default what uris;
+     {status with moo_content_rev =
+        (TacticAstPp.pp_command cmd ^ "\n") :: status.moo_content_rev}
   | TacticAst.Include (loc, path) ->
      let path = MatitaMisc.obj_file_of_script path in
      let stream = Stream.of_channel (open_in path) in
@@ -536,13 +540,14 @@ and disambiguate_tacticals status tacticals =
   status, tacticals
   
 let disambiguate_command status = function
-  | TacticAst.Include (loc,path) as cmd  -> status,cmd
+  | TacticAst.Default _
+  | TacticAst.Alias _
+  | TacticAst.Include _ as cmd  -> status,cmd
   | TacticAst.Coercion (loc, term) ->
       let status, term = disambiguate_term status term in
       status, TacticAst.Coercion (loc,term)
   | (TacticAst.Set _ | TacticAst.Qed _ | TacticAst.Drop _ ) as cmd ->
       status, cmd
-  | TacticAst.Alias _ as x -> status, x
   | TacticAst.Obj (loc,obj) ->
       let status,obj = disambiguate_obj status obj in
        status, TacticAst.Obj (loc,obj)