diff options
author | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
commit | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch) | |
tree | 97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /proofs/clenvtac.ml | |
parent | 300293c119981054c95182a90c829058530a6b6f (diff) |
Imported Upstream version 8.4~betaupstream/8.4_beta
Diffstat (limited to 'proofs/clenvtac.ml')
-rw-r--r-- | proofs/clenvtac.ml | 38 |
1 files changed, 21 insertions, 17 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 7b760859..eb935d05 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-2010 *) (* \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))); @@ -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,27 @@ 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; + 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 = |