From e1d3db51fb0d63c882c0a40d9b91bc28ab05747e Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 5 Sep 2003 16:23:17 +0000 Subject: [PATCH] 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. --- helm/ocaml/cic_omdoc/content2cic.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) 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 -> -- 2.39.2