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 d700ddd07cf8e5da6ab0d914ac1a3d0b90bcd416..90ce050e34e1fbb2db42df1c946439b61ede3f93 100644 (file)
--- 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 a509bbb8da525c531c70e966b0c415533fab555d..fd37443965f85594e5cde7e491924c8133155954 100644 (file)
--- 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 df8f484ba211a6f327614e805cd8f9f7d1ae19cf..cb420d267ecf41f866a96dcb2695d1a95a93c00f 100644 (file)
--- 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)