From: Stefano Zacchiroli Date: Fri, 5 Sep 2003 16:23:17 +0000 (+0000) Subject: Defs in context may now have an optional type (when unknown). X-Git-Tag: v0_0_1~27 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=e1d3db51fb0d63c882c0a40d9b91bc28ab05747e;p=helm.git Defs in context may now have an optional type (when unknown). During type-checking, LetIn are pushed in the context as Defs with a known type. When a Rel pointing to a Def in the context is found, the already computed type (if present) is used instead of re-typing the body of the LetIn. As a result, we get a (possibly exponential) decrease in the complexity of the typing algorithm. --- diff --git a/helm/ocaml/cic_omdoc/content2cic.ml b/helm/ocaml/cic_omdoc/content2cic.ml index ed62e254c..65ea0d306 100644 --- a/helm/ocaml/cic_omdoc/content2cic.ml +++ b/helm/ocaml/cic_omdoc/content2cic.ml @@ -149,7 +149,10 @@ let proof2cic deannotate p = (match conclude.Con.conclude_args with [Con.ArgProof p] -> proof2cic [] p (* empty! *) | _ -> prerr_endline "4"; assert false) - else if (conclude.Con.conclude_method = "ByInduction") then + else if (conclude.Con.conclude_method = "ByInduction" || + conclude.Con.conclude_method = "AndInd" || + conclude.Con.conclude_method = "Exists" || + conclude.Con.conclude_method = "FalseInd") then (match (List.tl conclude.Con.conclude_args) with Con.Term (C.AAppl id ((C.AConst(idc,uri,exp_named_subst))::params_and_IP))::args ->