diff options
Diffstat (limited to 'contrib')
-rw-r--r-- | contrib/xml/cic2acic.ml | 16 |
1 files changed, 15 insertions, 1 deletions
diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml index ec5ccc8e5..b15611438 100644 --- a/contrib/xml/cic2acic.ml +++ b/contrib/xml/cic2acic.ml @@ -396,7 +396,21 @@ print_endline "ENVIRONMENT:" ; flush stdout ; Pp.ppnl (Printer.pr_context_of env) ; flush stdout ; print_endline "FINE_ENVIRONMENT" ; flush stdout ; *) - let innersort = get_sort_family_of env evar_map synthesized in + let innersort = + let synthesized_innersort = + get_sort_family_of env evar_map synthesized + in + match expected with + None -> synthesized_innersort + | Some ty -> + let expected_innersort = + get_sort_family_of env evar_map ty + in + match expected_innersort, synthesized_innersort with + CProp, _ + | _, CProp -> CProp + | _, _ -> expected_innersort + in (* Debugging only: print_endline "PASSATO" ; flush stdout ; *) |