diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-09-11 20:00:27 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-09-12 10:39:32 +0200 |
| commit | ca300977724a6b065a98c025d400c71f41b9df4b (patch) | |
| tree | 59a2fd3327b3d0eb9cd1e11cbb31605f2a08ea27 /pretyping/pretyping.ml | |
| parent | 012fe1a96ba81ab0a7fa210610e3f25187baaf1d (diff) | |
Parsing evar instances.
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index f26d2d638..a21548d57 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -407,7 +407,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var (pretype_id (fun e r l t -> pretype tycon e r l t) loc env evdref lvar id) tycon - | GEvar (loc, id, instopt) -> + | GEvar (loc, id, inst) -> (* Ne faudrait-il pas s'assurer que hyps est bien un sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *) let evk = @@ -415,9 +415,9 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var with Not_found -> user_err_loc (loc,"",str "Unknown existential variable.") in let hyps = evar_filtered_context (Evd.find !evdref evk) in - let args = match instopt with - | None -> Array.of_list (instance_from_named_context hyps) - | Some inst -> error "Non-identity subtitutions of existential variables not implemented" in + let f c = (pretype empty_tycon env evdref lvar c).uj_val in + let inst = List.map (on_snd f) inst in + let args = complete_instance hyps inst in let c = mkEvar (evk, args) in let j = (Retyping.get_judgment_of env !evdref c) in inh_conv_coerce_to_tycon loc env evdref j tycon |