diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/micromega/coq_micromega.ml | 4 | ||||
| -rw-r--r-- | contrib/subtac/subtac_coercion.ml | 30 |
2 files changed, 14 insertions, 20 deletions
diff --git a/contrib/micromega/coq_micromega.ml b/contrib/micromega/coq_micromega.ml index 02ff61a1..5ae12394 100644 --- a/contrib/micromega/coq_micromega.ml +++ b/contrib/micromega/coq_micromega.ml @@ -1193,8 +1193,8 @@ let call_csdpcert provername poly = output_value ch_to (provername,poly : provername * micromega_polys); close_out ch_to; let cmdname = - Filename.concat Coq_config.bindir - ("csdpcert" ^ Coq_config.exec_extension) in + List.fold_left Filename.concat Coq_config.coqlib + ["contrib"; "micromega"; "csdpcert" ^ Coq_config.exec_extension] in let c = Sys.command (cmdname ^" "^ tmp_to ^" "^ tmp_from) in (try Sys.remove tmp_to with _ -> ()); if c <> 0 then Util.error ("Failed to call csdp certificate generator"); diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml index b046f0b3..4d8f868f 100644 --- a/contrib/subtac/subtac_coercion.ml +++ b/contrib/subtac/subtac_coercion.ml @@ -6,7 +6,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac_coercion.ml 11282 2008-07-28 11:51:53Z msozeau $ *) +(* $Id: subtac_coercion.ml 11343 2008-09-01 20:55:13Z herbelin $ *) open Util open Names @@ -310,8 +310,6 @@ module Coercion = struct (* Typing operations dealing with coercions *) - let class_of1 env sigma t = class_of env sigma (nf_evar sigma t) - (* Here, funj is a coercion therefore already typed in global context *) let apply_coercion_args env argl funj = let rec apply_rec acc typ = function @@ -339,19 +337,17 @@ module Coercion = struct (* raise Not_found if no coercion found *) let inh_pattern_coerce_to loc pat ind1 ind2 = - let i1 = inductive_class_of ind1 in - let i2 = inductive_class_of ind2 in - let p = lookup_pattern_path_between (i1,i2) in + let p = lookup_pattern_path_between (ind1,ind2) in apply_pattern_coercion loc pat p (* appliquer le chemin de coercions p à hj *) - let apply_coercion env p hj typ_cl = + let apply_coercion env sigma p hj typ_cl = try fst (List.fold_left (fun (ja,typ_cl) i -> let fv,isid = coercion_value i in - let argl = (class_args_of typ_cl)@[ja.uj_val] in + let argl = (class_args_of env sigma typ_cl)@[ja.uj_val] in let jres = apply_coercion_args env argl fv in (if isid then { uj_val = ja.uj_val; uj_type = jres.uj_type } @@ -370,9 +366,9 @@ module Coercion = struct (isevars',{ uj_val = j.uj_val; uj_type = t }) | _ -> (try - let t,i1 = class_of1 env (evars_of isevars) j.uj_type in - let p = lookup_path_to_fun_from i1 in - (isevars,apply_coercion env p j t) + let t,p = + lookup_path_to_fun_from env (evars_of isevars) j.uj_type in + (isevars,apply_coercion env (evars_of isevars) p j t) with Not_found -> try let coercef, t = mu env isevars t in @@ -382,9 +378,8 @@ module Coercion = struct let inh_tosort_force loc env isevars j = try - let t,i1 = class_of1 env (evars_of isevars) j.uj_type in - let p = lookup_path_to_sort_from i1 in - let j1 = apply_coercion env p j t in + let t,p = lookup_path_to_sort_from env (evars_of isevars) j.uj_type in + let j1 = apply_coercion env (evars_of isevars) p j t in (isevars,type_judgment env (j_nf_evar (evars_of isevars) j1)) with Not_found -> error_not_a_type_loc loc env (evars_of isevars) j @@ -417,12 +412,11 @@ module Coercion = struct else let v', t' = try - let t1,i1 = class_of1 env (evars_of evd) c1 in - let t2,i2 = class_of1 env (evars_of evd) t in - let p = lookup_path_between (i2,i1) in + let t2,t1,p = lookup_path_between env (evars_of evd) (t,c1) in match v with Some v -> - let j = apply_coercion env p {uj_val = v; uj_type = t} t2 in + let j = apply_coercion env (evars_of evd) p + {uj_val = v; uj_type = t} t2 in Some j.uj_val, j.uj_type | None -> None, t with Not_found -> raise NoCoercion |