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 ec9dc680e376c0a3ae0ddbf888775d6ad208501b..1861ce5b0222e132d53d72f08474f471f6bbbbfc 100644 (file)
--- 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