diff options
Diffstat (limited to 'contrib/xml/cic2acic.ml')
| -rw-r--r-- | contrib/xml/cic2acic.ml | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml index 1a6cb9c8..c62db00b 100644 --- a/contrib/xml/cic2acic.ml +++ b/contrib/xml/cic2acic.ml @@ -349,7 +349,7 @@ let source_id_of_id id = "#source#" ^ id;; let acic_of_cic_context' computeinnertypes seed ids_to_terms constr_to_ids ids_to_father_ids ids_to_inner_sorts ids_to_inner_types - pvars ?(fake_dependent_products=false) env idrefs evar_map t expectedty + ?(fake_dependent_products=false) env idrefs evar_map t expectedty = let module D = DoubleTypeInference in let module E = Environ in @@ -541,6 +541,8 @@ print_endline "PASSATO" ; flush stdout ; add_inner_type fresh_id'' ; A.ARel (fresh_id'', n, List.nth idrefs (n-1), id) | T.Var id -> + let pvars = Termops.ids_of_named_context (E.named_context env) in + let pvars = List.map N.string_of_id pvars in let path = get_uri_of_var (N.string_of_id id) pvars in Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; if is_a_Prop innersort && expected_available then @@ -827,6 +829,7 @@ print_endline "PASSATO" ; flush stdout ; aux computeinnertypes None [] env idrefs t ;; +(* Obsolete [HH 1/2009] let acic_of_cic_context metasenv context t = let ids_to_terms = Hashtbl.create 503 in let constr_to_ids = Acic.CicHash.create 503 in @@ -838,8 +841,9 @@ let acic_of_cic_context metasenv context t = ids_to_inner_sorts ids_to_inner_types metasenv context t, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, ids_to_inner_types ;; +*) -let acic_object_of_cic_object pvars sigma obj = +let acic_object_of_cic_object sigma obj = let module A = Acic in let ids_to_terms = Hashtbl.create 503 in let constr_to_ids = Acic.CicHash.create 503 in @@ -853,7 +857,7 @@ let acic_object_of_cic_object pvars sigma obj = let seed = ref 0 in let acic_term_of_cic_term_context' = acic_of_cic_context' true seed ids_to_terms constr_to_ids ids_to_father_ids - ids_to_inner_sorts ids_to_inner_types pvars in + ids_to_inner_sorts ids_to_inner_types in (*CSC: is this the right env to use? Hhmmm. There is a problem: in *) (*CSC: Global.env () the object we are exporting is already defined, *) (*CSC: either in the environment or in the named context (in the case *) |