diff options
Diffstat (limited to 'contrib/xml')
| -rw-r--r-- | contrib/xml/cic2acic.ml | 4 | ||||
| -rw-r--r-- | contrib/xml/doubleTypeInference.ml | 20 |
2 files changed, 19 insertions, 5 deletions
diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml index a6b2eaf00..767790b87 100644 --- a/contrib/xml/cic2acic.ml +++ b/contrib/xml/cic2acic.ml @@ -359,7 +359,9 @@ let acic_of_cic_context' computeinnertypes seed ids_to_terms constr_to_ids in let ainnertypes,innertype,innersort,expected_available = let {D.synthesized = synthesized; D.expected = expected} = - if computeinnertypes then + if computeinnertypes + || (match Term.kind_of_term tt with Term.Sort _ -> false | _ -> true) + then try Acic.CicHash.find terms_to_types tt with _ -> diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml index 3c5362509..6337506e7 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' = Reductionops.nf_beta synthesized in + let synthesized' = Unshare.unshare (Reductionops.nf_beta synthesized) in let types,res = match expectedty with None -> @@ -251,14 +251,26 @@ 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 expectedty'}, + {synthesized = synthesized' ; expected = Some (Unshare.unshare 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 ; - E.make_judge cstr res + 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 and execute_recdef env sigma (names,lar,vdef) = |