- recent changes to doubleTypeInference.ml (that introduced double

  type inference for inferred types) undone. Previous performance restored.
- bug in cic2acic (code that used to be dead fixed): the type of a sort
  was computed as the sort itself
- CPropRetyping in cic2acic modified to handle correctly the sort Set in
  the two cases Predicative Set / Impredicative Set
- CPropRetyping.get_type_of used in place of Retyping.get_type_of everywhere
  in cic2acic. This closes (again, but more efficiently) the bug about
  CProps erroneously recognized as Types in inferred types


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5875 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 4 insertions, 16 deletions

diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml
index 6337506e70..3c53625090 100644
--- a/contrib/xml/doubleTypeInference.ml
+++ b/contrib/xml/doubleTypeInference.ml
@@ -165,7 +165,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
 (try
         Typeops.judge_of_type u
  with _ -> (* Successor of a non universe-variable universe anomaly *)
- (*(Pp.ppnl (Pp.str "Warning: universe refresh performed!!!") ; flush stdout ) ;*)
+ (Pp.ppnl (Pp.str "Warning: universe refresh performed!!!") ; flush stdout ) ;
   Typeops.judge_of_type (Termops.new_univ ())
 )
 
@@ -238,7 +238,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
 	 j
     in
      let synthesized = E.j_type judgement in
-     let synthesized' = Unshare.unshare (Reductionops.nf_beta synthesized) in
+     let synthesized' = Reductionops.nf_beta synthesized in
       let types,res =
        match expectedty with
           None ->
@@ -251,26 +251,14 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
            (* the synthesized type. Let's forget it.       *)
            {synthesized = synthesized' ; expected = None}, synthesized
         | Some expectedty' ->
-           {synthesized = synthesized' ; expected = Some (Unshare.unshare expectedty')},
+           {synthesized = synthesized' ; expected = Some expectedty'},
            expectedty'
       in
 (*CSC: debugging stuff to be removed *)
 if Acic.CicHash.mem subterms_to_types cstr then
  (Pp.ppnl (Pp.(++) (Pp.str "DUPLICATE INSERTION: ") (Printer.prterm cstr)) ; flush stdout ) ;
        Acic.CicHash.add subterms_to_types cstr types ;
-       let recur_on_type ty =
-        match Term.kind_of_term ty with
-           Term.Sort _ -> ()
-         | _ ->
-           ignore (execute env sigma ty None)
-       in
-        recur_on_type types.synthesized ;
-        begin
-         match types.expected with
-            None -> ()
-          | Some ty -> recur_on_type ty
-        end ;
-        E.make_judge cstr res
+       E.make_judge cstr res
 
 
  and execute_recdef env sigma (names,lar,vdef) =