overload resolution with value type, for experiment

3 files changed, 15 insertions, 15 deletions

diff --git a/examples/logic/ArithmEng.gf b/examples/logic/ArithmEng.gf
index 05526b365..1ab4c2abd 100644
--- a/examples/logic/ArithmEng.gf
+++ b/examples/logic/ArithmEng.gf
@@ -29,15 +29,15 @@ lin
 
   evax1 = 
     proof (by (ref (mkLabel ["the first axiom of evenness ,"]))) 
-      (mkS (pred (regA "even") (UsePN (regPN "zero")))) ;
+      (mkS (predA (regA "even") (UsePN (regPN "zero")))) ;
   evax2 n c = 
     appendText c 
       (proof (by (ref (mkLabel ["the second axiom of evenness ,"]))) 
-        (mkS (pred (regA "odd") (appN2 (regN2 "successor") n)))) ;
+        (mkS (predA (regA "odd") (appN2 (regN2 "successor") n)))) ;
   evax3 n c = 
     appendText c 
       (proof (by (ref (mkLabel ["the third axiom of evenness ,"]))) 
-        (mkS (pred (regA "even") (appN2 (regN2 "successor") n)))) ;
+        (mkS (predA (regA "even") (appN2 (regN2 "successor") n)))) ;
 
 
   eqax1 = 
diff --git a/examples/logic/LogicI.gf b/examples/logic/LogicI.gf
index f8eaf6aa2..1f9b08e41 100644
--- a/examples/logic/LogicI.gf
+++ b/examples/logic/LogicI.gf
@@ -18,9 +18,9 @@ lincat
 lin
   ThmWithProof = theorem ;
 
-  Conj A = coord and_Conj A ;
-  Disj A B = coord or_Conj A B ;
-  Impl A B = coord ifthen_DConj A B ;
+  Conj = coord and_Conj ;
+  Disj = coord or_Conj ;
+  Impl = coord ifthen_DConj ;
 
   Abs = 
     mkS (pred have_V2 (mkNP we_Pron) (mkNP (mkDet IndefArt) contradiction_N)) ;
@@ -28,21 +28,21 @@ lin
   Univ A B = 
     AdvS 
       (mkAdv for_Prep (mkNP all_Predet 
-        (mkNP (mkDet (PlQuant IndefArt)) (mkCN A (symb B.$0)))))
+        (mkNP (mkDet (PlQuant IndefArt) NoNum NoOrd) (mkCN A (symb B.$0)))))
       B ;
 
   DisjIl A B a = proof a (proof afortiori (coord or_Conj A B)) ;
   DisjIr A B b = proof b (proof afortiori (coord or_Conj A B)) ;
 
-  DisjE A B C c b1 b2 =
+  DisjE A B C c d e =
     appendText
       c 
       (appendText
         (appendText
            (cases (mkNum n2)) 
            (proofs 
-             (appendText (assumption A) b1)
-             (appendText (assumption B) b2)))
+             (appendText (assumption A) d)
+             (appendText (assumption B) e)))
         (proof therefore C)) ;
 
   ImplI A B b = 
diff --git a/examples/logic/Prooftext.gf b/examples/logic/Prooftext.gf
index 3a5a61894..4c193740a 100644
--- a/examples/logic/Prooftext.gf
+++ b/examples/logic/Prooftext.gf
@@ -32,7 +32,7 @@ oper
 
   definition : Decls -> Object -> Object -> Section 
     = \decl,a,b -> 
-        appendText decl (mkUtt (mkS (pred b a))) ;
+        appendText decl (mkText (mkPhr (mkUtt (mkS (pred b a)))) TEmpty) ;
 
   theorem : Prop -> Proof -> Section 
     = \prop,prf -> appendText (mkText (mkPhr prop) TEmpty) prf ;
@@ -64,17 +64,17 @@ oper
     = appendText ;
 
   cases : Num -> Branching 
-    = \nu -> 
-        mkS (pred have_V2 (mkNP we_Pron) (mkNP (mkDet nu) case_N)) ;
+    = \n -> 
+        mkS (pred have_V2 (mkNP we_Pron) (mkNP (mkDet n) case_N)) ;
 
   by : Ref -> Adverb 
-    = \h -> mkAdv by8means_Prep h ;
+    = \h -> C.mkPConj (mkAdv by8means_Prep h).s ;
   therefore : Adverb
     = therefore_PConj ;
   afortiori : Adverb
     = C.mkPConj ["a fortiori"] ;
   hypothesis : Adverb
-    = mkAdv by8means_Prep (mkNP (mkDet DefArt) hypothesis_N) ;
+    = C.mkPConj (mkAdv by8means_Prep (mkNP (mkDet DefArt) hypothesis_N)).s ;
 
   ref : Label -> Ref
     = \h -> h ;