From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 29 Apr 2002 10:22:09 +0000 (+0000)
Subject: Computed inner-types are now also put in whd normal form.
X-Git-Tag: V_0_3_0_debian_8~119
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=2a40efede6d4430b4ca086275bcac80905ec1a74

Computed inner-types are now also put in whd normal form.
This is at the same type too strong (e.g. it performs delta-reductions)
and too weak (it is not full-reduction).
We can consider this just a patch waiting for Coscoy's double-inference
algorithm implementation.
---

diff --git a/helm/gTopLevel/cic2acic.ml b/helm/gTopLevel/cic2acic.ml
index ec9dc680e..1861ce5b0 100644
--- a/helm/gTopLevel/cic2acic.ml
+++ b/helm/gTopLevel/cic2acic.ml
@@ -70,7 +70,12 @@ let acic_of_cic_env' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
      in
       let ainnertype,innertype,innersort =
        let cicenv = List.map (function (_,ty) -> ty) bs in
-        let innertype = T.type_of_aux' metasenv cicenv tt in
+(*CSC: Here we need the algorithm for Coscoy's double type-inference  *)
+(*CSC: (expected type + inferred type). Just for now we use the usual *)
+(*CSC: type-inference, but the result is very poort. As a very weak   *)
+(*CSC: patch, I apply whd to the computed type. Full beta             *)
+(*CSC: reduction would be a much better option.                       *)
+        let innertype = CicReduction.whd (T.type_of_aux' metasenv cicenv tt) in
          let innersort = T.type_of_aux' metasenv cicenv innertype in
           let ainnertype =
            if computeinnertypes then