From: Stefano Zacchiroli <zack@upsilon.cc>
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;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 ->