- Procedural: we now check that an eliminator opens as many goals as the ...

              So nat_double_ind is not an eliminator for Nat :)
- Base-2    : now compiles correctly because we fixed the preamble :)

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index e71f443d9cefa3c79fb87a2294099270cab019ed..b37eef6bbc989034b8dbe2e7fd851dc454baf943 100644 (file)
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -347,20 +347,24 @@ and proc_appl st what hd tl =
       let script = List.rev (mk_arg st hd) in
       match rc with
          | Some (i, j, uri, tyno) ->
-           let classes, tl, _, where = split2_last classes tl in
-           let script = List.rev (mk_arg st where) @ script in
-           let synth = I.S.add 1 synth in
+           let classes2, tl2, _, where = split2_last classes tl in
+           let script2 = List.rev (mk_arg st where) @ script in
+           let synth2 = I.S.add 1 synth in
            let names = get_ind_names uri tyno in
-           let qs = proc_bkd_proofs (next st) synth names classes tl in
-            if is_rewrite_right hd then 
-              script @ mk_rewrite st dtext where qs tl false what
+           let qs = proc_bkd_proofs (next st) synth2 names classes2 tl2 in
+            if List.length qs <> List.length names then
+              let qs = proc_bkd_proofs (next st) synth [] classes tl in
+              let hd = mk_exp_args hd tl classes synth in
+              script @ [T.Apply (hd, dtext ^ text); T.Branch (qs, "")]
+           else if is_rewrite_right hd then 
+              script2 @ mk_rewrite st dtext where qs tl2 false what
            else if is_rewrite_left hd then 
-              script @ mk_rewrite st dtext where qs tl true what
+              script2 @ mk_rewrite st dtext where qs tl2 true what
            else
-              let predicate = List.nth tl (parsno - i) in
+              let predicate = List.nth tl2 (parsno - i) in
                let e = Cn.mk_pattern j predicate in
               let using = Some hd in
-              (* convert_elim st what what e @ *) script @ 
+              (* convert_elim st what what e @ *) script2 @ 
               [T.Elim (where, using, e, dtext ^ text); T.Branch (qs, "")]
         | None        ->
            let qs = proc_bkd_proofs (next st) synth [] classes tl in

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/preamble.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/preamble.ma
index 114efbd53479edff13a2103421c2283d46a30219..c2c93f32306e87b10ecdd63f168b7f0c7f72f15e 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/preamble.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/preamble.ma
@@ -14,6 +14,3 @@
 
 include "Base-1/definitions.ma".
 include "Legacy-2/theory.ma".
-
-alias symbol "minus" = "Coq's natural minus".
-alias symbol "lt" = "Coq's natural 'less than'".

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Makefile b/helm/software/matita/contribs/LAMBDA-TYPES/Makefile
index a5bf300152540a9a1c0a3ab72a57a06ac08947c1..fb55d67825a0e66712a1a6e783b68115692d1eeb 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Makefile
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Makefile
@@ -6,8 +6,7 @@ MATITAOPTIONS=$(MATITAUSEROPTIONS) -onepass
 
 DIR=$(shell basename $$PWD)
 
-MMAS = $(shell find Legacy-2 -name "*.mma")
-# Base-2 
+MMAS = $(shell find Legacy-2 Base-2 -name "*.mma") 
 MAS = $(MMAS:%.mma=%.ma)
 XMAS = Legacy-2/theory.ma Base-2/theory.ma LambdaDelta-2/theory.ma
 
@@ -19,13 +18,13 @@ $(DIR).opt opt all.opt: depends
 
 build: $(MAS)
        $(H)echo Legacy-2/theory.ma `$(BIN)matitadep.opt -stdout Legacy-2/theory.ma` >> depends
-#      $(H)echo Base-2/theory.ma `$(BIN)matitadep.opt -stdout Base-2/theory.ma` >> depends
+       $(H)echo Base-2/theory.ma `$(BIN)matitadep.opt -stdout Base-2/theory.ma` >> depends
        $(H)$(BIN)matitac $(MATITAOPTIONS) 2> /dev/null
        $(H)rm depends
 
 build.opt: $(MAS)
        $(H)echo Legacy-2/theory.ma `$(BIN)matitadep.opt -stdout Legacy-2/theory.ma` >> depends
-#      $(H)echo Base-2/theory.ma `$(BIN)matitadep.opt -stdout Base-2/theory.ma` >> depends
+       $(H)echo Base-2/theory.ma `$(BIN)matitadep.opt -stdout Base-2/theory.ma` >> depends
        $(H)$(BIN)matitac.opt $(MATITAOPTIONS) 2> /dev/null
        $(H)rm depends
 
@@ -44,14 +43,12 @@ clean.ma:
 depend:
        @echo matitadep
        $(H)$(BIN)matitadep $(foreach FILE,$(XMAS),-exclude $(FILE))
-       $(H)cat Legacy-2/depends >> depends
-# Base-2/depends
+       $(H)cat Legacy-2/depends Base-2/depends >> depends
        
 depend.opt:
        @echo matitadep.opt
        $(H)$(BIN)matitadep.opt $(foreach FILE,$(XMAS),-exclude $(FILE))
-       $(H)cat Legacy-2/depends >> depends
-# Base-2/depends
+       $(H)cat Legacy-2/depends Base-2/depends >> depends
 
 depends: depend.opt
 
@@ -61,4 +58,4 @@ depends: depend.opt
        $(H)echo $@ `$(BIN)matitadep.opt -stdout $@` >> depends
 
 include Legacy-2/.depend
-# include Base-2/.depend
+include Base-2/.depend