diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 4 | ||||
| -rw-r--r-- | pretyping/evarconv.ml | 2 | ||||
| -rw-r--r-- | pretyping/evarutil.ml | 2 | ||||
| -rw-r--r-- | pretyping/evarutil.mli | 2 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 5 |
5 files changed, 8 insertions, 7 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index ad02ce58b..67bdfbbcf 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -20,7 +20,7 @@ open Evarutil (* This was previously in Indrec but creates existential holes *) let mkExistential isevars env = - let (c,_) = new_isevar isevars env (mkCast dummy_sort dummy_sort) CCI in c + new_isevar isevars env (mkCast dummy_sort dummy_sort) CCI let norec_branch_scheme env isevars typc = let rec crec typc = match whd_betadeltaiota env !isevars typc with @@ -789,7 +789,7 @@ let inh_coerce_to_ind isevars env ty tyi = (fun (na,ty) (env,evl) -> let s = get_sort_of env Evd.empty ty in (push_rel (na,(make_typed ty s)) env, - fst (new_isevar isevars env (mkCast ty (mkSort s)) CCI)::evl)) + (new_isevar isevars env (mkCast ty (mkSort s)) CCI)::evl)) ntys (env,[]) in let expected_typ = applist (mkMutInd tyi,evarl) in (* devrait être indifférent d'exiger leq ou pas puisque pour diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index d80810af5..539a953a1 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -324,7 +324,7 @@ and conv_record env isevars (c,bs,(xs,xs1),(us,us1),(ts,ts1),t) = let ks = List.fold_left (fun ks b -> - let (k,_) = new_isevar isevars env (substl ks b) CCI in (k::ks)) + (new_isevar isevars env (substl ks b) CCI)::ks) [] bs in if (list_for_all2eq diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 38edd1e32..87fd80963 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -220,7 +220,7 @@ let new_isevar isevars env typ k = let (sigma',evar) = new_isevar_sign env' !isevars typ' (Array.of_list newargs) in isevars := sigma'; - (evar,typ') + evar diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 03982044e..0758210b1 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -35,7 +35,7 @@ val ise_defined : 'a evar_defs -> constr -> bool val real_clean : 'a evar_defs -> int -> (identifier * constr) list -> constr -> constr val new_isevar : - 'a evar_defs -> env -> constr -> path_kind -> constr * constr + 'a evar_defs -> env -> constr -> path_kind -> constr val evar_define : 'a evar_defs -> constr -> constr -> int list val solve_simple_eqn : (constr -> constr -> bool) -> 'a evar_defs -> (conv_pb * constr * constr) -> int list option diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 2ccb6c94b..02742b64c 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -298,10 +298,11 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *) let (valc,typc) = (body_of_type v,mkSort (level_of_type v)) in {uj_val=valc; uj_type=typc; uj_kind=dummy_sort} | (false,(None,Some ty)) -> - let (c,ty) = new_isevar isevars env ty CCI in + let c = new_isevar isevars env ty CCI in {uj_val=c;uj_type=ty;uj_kind = dummy_sort} | (true,(None,None)) -> - let (c,ty) = new_isevar isevars env (mkCast dummy_sort dummy_sort) CCI in + let ty = mkCast dummy_sort dummy_sort in + let c = new_isevar isevars env ty CCI in {uj_val=c;uj_type=ty;uj_kind = dummy_sort} | (false,(None,None)) -> (match loc with |