Thanks, Vincent! I definitely have to work your exercise now. Two dumb questions: 1) how do I get quotexpander to turn off type inference by putting a period at the end of the terms? Of all your possibilities, that's the one I like best. 2)Doesn't Ocaml use the "applicative order application" so that if I type cases "case_string" [`t1`; `t2`; `t3`];; that I can not defined cases by let case str termlist = let quotexpander = .... [do the cases construction] let quotexpander = original version of quotexpander;; Because Ocaml will evaluate all the arguments independently?
Petros, your consider and *rule_tac tactics code looks excellent! I noticed one simple thing: X_GEN_TAC in tactics.ml also uses type_of to infer types. It's a dumb of me, but I didn't think you could use type_of in Ocaml code. -- Best, Bill ------------------------------------------------------------------------------ Minimize network downtime and maximize team effectiveness. Reduce network management and security costs.Learn how to hire the most talented Cisco Certified professionals. Visit the Employer Resources Portal http://www.cisco.com/web/learning/employer_resources/index.html _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
