diff options
Diffstat (limited to 'plugins/subtac/subtac_pretyping.ml')
| -rw-r--r-- | plugins/subtac/subtac_pretyping.ml | 26 |
1 files changed, 16 insertions, 10 deletions
diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml index 030bb3c5..23323ab3 100644 --- a/plugins/subtac/subtac_pretyping.ml +++ b/plugins/subtac/subtac_pretyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: subtac_pretyping.ml 13344 2010-07-28 15:04:36Z msozeau $ *) open Global open Pp @@ -70,7 +70,7 @@ let merge_evms x y = let interp env isevars c tycon = let j = pretype tycon env isevars ([],[]) c in let _ = isevars := Evarutil.nf_evar_map !isevars in - let evd,_ = consider_remaining_unif_problems env !isevars in + let evd = consider_remaining_unif_problems env !isevars in (* let unevd = undefined_evars evd in *) let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:true ~split:true ~fail:true env evd in let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:false ~split:true ~fail:false env unevd' in @@ -86,8 +86,10 @@ let find_with_index x l = open Vernacexpr -let coqintern_constr evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_constr ( evd) env -let coqintern_type evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_type ( evd) env +let coqintern_constr evd env : Topconstr.constr_expr -> Rawterm.rawconstr = + Constrintern.intern_constr evd env +let coqintern_type evd env : Topconstr.constr_expr -> Rawterm.rawconstr = + Constrintern.intern_type evd env let env_with_binders env isevars l = let rec aux ((env, rels) as acc) = function @@ -109,21 +111,25 @@ let env_with_binders env isevars l = | [] -> acc in aux (env, []) l -let subtac_process env isevars id bl c tycon = +let subtac_process ?(is_type=false) env isevars id bl c tycon = let c = Topconstr.abstract_constr_expr c bl in - let tycon = + let tycon, imps = match tycon with - None -> empty_tycon + None -> empty_tycon, None | Some t -> let t = Topconstr.prod_constr_expr t bl in let t = coqintern_type !isevars env t in + let imps = Implicit_quantifiers.implicits_of_rawterm t in let coqt, ttyp = interp env isevars t empty_tycon in - mk_tycon coqt + mk_tycon coqt, Some imps in let c = coqintern_constr !isevars env c in - let imps = Implicit_quantifiers.implicits_of_rawterm c in + let imps = match imps with + | Some i -> i + | None -> Implicit_quantifiers.implicits_of_rawterm ~with_products:is_type c + in let coqc, ctyp = interp env isevars c tycon in - let evm = non_instanciated_map env isevars ( !isevars) in + let evm = non_instanciated_map env isevars !isevars in let ty = nf_evar !isevars (match tycon with Some (None, c) -> c | _ -> ctyp) in evm, coqc, ty, imps |