diff options
Diffstat (limited to 'plugins/subtac/subtac_pretyping.ml')
| -rw-r--r-- | plugins/subtac/subtac_pretyping.ml | 23 |
1 files changed, 9 insertions, 14 deletions
diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml index 9de7ddf2..fac6b567 100644 --- a/plugins/subtac/subtac_pretyping.ml +++ b/plugins/subtac/subtac_pretyping.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac_pretyping.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - open Global open Pp open Util @@ -26,7 +24,7 @@ open List open Recordops open Evarutil open Pretype_errors -open Rawterm +open Glob_term open Evarconv open Pattern @@ -60,20 +58,17 @@ let my_print_rec_info env t = str "Wf proof: " ++ my_print_constr env t.wf_proof ++ spc () ++ str "Abbreviated Type: " ++ my_print_constr env t.f_type ++ spc () ++ str "Full type: " ++ my_print_constr env t.f_fulltype -(* trace (str "pretype for " ++ (my_print_rawconstr env c) ++ *) +(* trace (str "pretype for " ++ (my_print_glob_constr env c) ++ *) (* str " and tycon "++ my_print_tycon env tycon ++ *) (* str " in environment: " ++ my_print_env env); *) -let merge_evms x y = - Evd.fold (fun ev evi evm -> Evd.add evm ev evi) 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 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 + let unevd' = Typeclasses.resolve_typeclasses ~filter:Subtac_utils.no_goals_or_obligations ~split:true ~fail:true env evd in + let unevd' = Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars ~split:true ~fail:false env unevd' in let evm = unevd' in isevars := unevd'; nf_evar evm j.uj_val, nf_evar evm j.uj_type @@ -86,9 +81,9 @@ let find_with_index x l = open Vernacexpr -let coqintern_constr evd env : Topconstr.constr_expr -> Rawterm.rawconstr = +let coqintern_constr evd env : Topconstr.constr_expr -> Glob_term.glob_constr = Constrintern.intern_constr evd env -let coqintern_type evd env : Topconstr.constr_expr -> Rawterm.rawconstr = +let coqintern_type evd env : Topconstr.constr_expr -> Glob_term.glob_constr = Constrintern.intern_type evd env let env_with_binders env isevars l = @@ -119,14 +114,14 @@ let subtac_process ?(is_type=false) env isevars id bl c tycon = | 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 imps = Implicit_quantifiers.implicits_of_glob_constr t in let coqt, ttyp = interp env isevars t empty_tycon in mk_tycon coqt, Some imps in let c = coqintern_constr !isevars env c in let imps = match imps with | Some i -> i - | None -> Implicit_quantifiers.implicits_of_rawterm ~with_products:is_type c + | None -> Implicit_quantifiers.implicits_of_glob_constr ~with_products:is_type c in let coqc, ctyp = interp env isevars c tycon in let evm = non_instanciated_map env isevars !isevars in |