diff options
author | Stephane Glondu <steph@glondu.net> | 2013-05-08 18:01:07 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2013-05-08 18:01:07 +0200 |
commit | 095eac936751bab72e3c6bbdfa3ede51f7198721 (patch) | |
tree | 44cf2859ba6b8486f056efaaf7ee6c2d855f2aae /proofs/clenvtac.ml | |
parent | 4e6d6dab2ef2de6c1ad7972fc981e55a4fde7ae3 (diff) | |
parent | 0b14713e3efd7f8f1cc8a06555d0ec8fbe496130 (diff) |
Merge branch 'experimental/master'
Diffstat (limited to 'proofs/clenvtac.ml')
-rw-r--r-- | proofs/clenvtac.ml | 43 |
1 files changed, 24 insertions, 19 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 7b760859..d18ee73f 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.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: clenvtac.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - open Pp open Util open Names @@ -20,12 +18,11 @@ open Evd open Evarutil open Proof_type open Refiner -open Proof_trees open Logic open Reduction open Reductionops open Tacmach -open Rawterm +open Glob_term open Pattern open Tacexpr open Clenv @@ -64,7 +61,7 @@ let clenv_value_cast_meta clenv = clenv_cast_meta clenv (clenv_value clenv) let clenv_pose_dependent_evars with_evars clenv = - let dep_mvs = clenv_dependent false clenv in + let dep_mvs = clenv_dependent clenv in if dep_mvs <> [] & not with_evars then raise (RefinerError (UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs))); @@ -74,8 +71,8 @@ let clenv_refine with_evars ?(with_classes=true) clenv gls = let clenv = clenv_pose_dependent_evars with_evars clenv in let evd' = if with_classes then - Typeclasses.resolve_typeclasses ~fail:(not with_evars) - clenv.env clenv.evd + Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars + ~fail:(not with_evars) clenv.env clenv.evd else clenv.evd in let clenv = { clenv with evd = evd' } in @@ -84,17 +81,18 @@ let clenv_refine with_evars ?(with_classes=true) clenv gls = (refine (clenv_cast_meta clenv (clenv_value clenv))) gls -let dft = Unification.default_unify_flags +open Unification + +let dft = default_unify_flags -let res_pf clenv ?(with_evars=false) ?(allow_K=false) ?(flags=dft) gls = - clenv_refine with_evars - (clenv_unique_resolver allow_K ~flags:flags clenv gls) gls +let res_pf clenv ?(with_evars=false) ?(flags=dft) gls = + clenv_refine with_evars (clenv_unique_resolver ~flags clenv gls) gls let elim_res_pf_THEN_i clenv tac gls = - let clenv' = (clenv_unique_resolver true clenv gls) in + let clenv' = (clenv_unique_resolver ~flags:elim_flags clenv gls) in tclTHENLASTn (clenv_refine false clenv') (tac clenv') gls -let e_res_pf clenv = res_pf clenv ~with_evars:true ~allow_K:false ~flags:dft +let e_res_pf clenv = res_pf clenv ~with_evars:true ~flags:dft (* [unifyTerms] et [unify] ne semble pas gérer les Meta, en @@ -102,21 +100,28 @@ let e_res_pf clenv = res_pf clenv ~with_evars:true ~allow_K:false ~flags:dft d'une même Meta sont compatibles. D'ailleurs le "fst" jette les metas provenant de w_Unify. (Utilisé seulement dans prolog.ml) *) -open Unification - let fail_quick_unif_flags = { modulo_conv_on_closed_terms = Some full_transparent_state; - use_metas_eagerly = false; + use_metas_eagerly_in_conv_on_closed_terms = false; modulo_delta = empty_transparent_state; + modulo_delta_types = full_transparent_state; + modulo_delta_in_merge = None; + check_applied_meta_types = false; resolve_evars = false; - use_evars_pattern_unification = false; + use_pattern_unification = false; + use_meta_bound_pattern_unification = true; (* ? *) + frozen_evars = ExistentialSet.empty; + restrict_conv_on_strict_subterms = false; (* ? *) + modulo_betaiota = false; + modulo_eta = true; + allow_K_in_toplevel_higher_order_unification = false } (* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *) let unifyTerms ?(flags=fail_quick_unif_flags) m n gls = let env = pf_env gls in let evd = create_goal_evar_defs (project gls) in - let evd' = w_unify false env CONV ~flags m n evd in + let evd' = w_unify env evd CONV ~flags m n in tclIDTAC {it = gls.it; sigma = evd'} let unify ?(flags=fail_quick_unif_flags) m gls = |