diff options
| author | ppedrot | 2013-08-04 16:51:23 +0000 |
|---|---|---|
| committer | ppedrot | 2013-08-04 16:51:23 +0000 |
| commit | d91e0f86111718bc3146a6925d6f39c53ee990f1 (patch) | |
| tree | d81de6d2eded5c99e1bfda2fcb009f8120bed4d8 /pretyping | |
| parent | 9fd3b0c4f47fd83ce2ded3864fe2074463151aca (diff) | |
Removing useless casts between arrays and lists.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16659 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/pretyping.ml | 2 | ||||
| -rw-r--r-- | pretyping/vnorm.ml | 3 |
2 files changed, 3 insertions, 2 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 61f618c409..265ba4b144 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -307,7 +307,7 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *) let hyps = evar_filtered_context (Evd.find !evdref evk) in let args = match instopt with - | None -> instance_from_named_context hyps + | None -> Array.of_list (instance_from_named_context hyps) | Some inst -> failwith "Evar subtitutions not implemented" in let c = mkEvar (evk, args) in let j = (Retyping.get_judgment_of env !evdref c) in diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 4b08f7517a..76587a3408 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Util open Names open Declarations open Term @@ -59,7 +60,7 @@ let type_constructor mind mib typ params = if nparams = 0 then ctyp else let _,ctyp = decompose_prod_n nparams ctyp in - substl (List.rev (Array.to_list params)) ctyp + substl (Array.rev_to_list params) ctyp |