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 ed62e254cc0b6a499560a48c1c63838273706504..65ea0d3069efc56f460ac632aefaf4590732531a 100644 (file)
--- 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 ->