summaryrefslogtreecommitdiff
path: root/contrib
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2008-09-08 00:15:04 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2008-09-08 00:15:04 +0200
commit113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (patch)
treec260a140410c796f113584a2f7e6b9b7f6e00aa5 /contrib
parent870075f34dd9fa5792bfbf413afd3b96f17e76a0 (diff)
Imported Upstream version 8.2~beta4.svn20080907+dfsgupstream/8.2.beta4.svn20080907+dfsg
Diffstat (limited to 'contrib')
-rw-r--r--contrib/micromega/coq_micromega.ml4
-rw-r--r--contrib/subtac/subtac_coercion.ml30
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