diff options
| -rw-r--r-- | dev/ocamldebug-coq.template | 3 | ||||
| -rw-r--r-- | dev/ocamlweb-doc/Makefile | 2 | ||||
| -rw-r--r-- | pretyping/evarutil.ml | 29 | ||||
| -rw-r--r-- | toplevel/mltop.ml4 | 5 |
4 files changed, 8 insertions, 31 deletions
diff --git a/dev/ocamldebug-coq.template b/dev/ocamldebug-coq.template index 31e928063..560d06d96 100644 --- a/dev/ocamldebug-coq.template +++ b/dev/ocamldebug-coq.template @@ -17,10 +17,9 @@ exec $OCAMLDEBUG \ -I $COQTOP/library -I $COQTOP/pretyping -I $COQTOP/parsing \ -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics \ -I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config \ - -I $COQTOP/translate \ -I $COQTOP/contrib/extraction -I $COQTOP/contrib/field \ -I $COQTOP/contrib/fourier -I $COQTOP/contrib/firstorder \ - -I $COQTOP/contrib/interface -I $COQTOP/contrib/jprover \ + -I $COQTOP/contrib/interface \ -I $COQTOP/contrib/omega -I $COQTOP/contrib/romega \ -I $COQTOP/contrib/ring -I $COQTOP/contrib/xml \ -I $COQTOP/contrib/subtac -I $COQTOP/contrib/funind \ diff --git a/dev/ocamlweb-doc/Makefile b/dev/ocamlweb-doc/Makefile index 7ab1bd3fc..f2c625ed4 100644 --- a/dev/ocamlweb-doc/Makefile +++ b/dev/ocamlweb-doc/Makefile @@ -8,7 +8,7 @@ LOCALINCLUDES=-I ../../config -I ../../tools -I ../../tools/coqdoc \ -I ../../contrib/ring -I ../../contrib/dp -I ../../contrib/setoid_ring \ -I ../../contrib/xml -I ../../contrib/extraction \ -I ../../contrib/interface -I ../../contrib/fourier \ - -I ../../contrib/jprover -I ../../contrib/cc \ + -I ../../contrib/cc \ -I ../../contrib/funind -I ../../contrib/firstorder \ -I ../../contrib/field -I ../../contrib/subtac -I ../../contrib/rtauto \ -I ../../contrib/recdef diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index b23c1cc60..6ac857d5c 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -978,7 +978,6 @@ let head_evar = that we don't care whether args itself contains Rel's or even Rel's distinct from the ones in l *) - let rec expand_and_check_vars env = function | [] -> [] | a::l -> @@ -991,35 +990,19 @@ let rec expand_and_check_vars env = function else raise Exit -(* -let is_identity_subst env args l = - let n = Array.length args in - (* Check named context from most recent to oldest declaration *) - let rec aux i = function - | [] -> i = 0 - | (id,_,_)::l -> args.(i) = mkVar id && aux (i-1) l in - (* Check named context from oldest to most recent declaration *) - let rec aux' i = function - | [] -> aux i (named_context env) - | _::l -> args.(i) = mkRel (n-i) && aux' (i-1) l in - List.for_all (fun c -> not (array_exists ((=) (expand_var env c)) args)) l && - aux' (n-1) (rel_context env) -*) - let is_unification_pattern_evar env (_,args) l t = -(* - (* Optimize the most common case *) - List.for_all (fun x -> isRel x || isVar x) l && is_identity_subst env args l - || -*) + List.for_all (fun x -> isRel x || isVar x) l (* common failure case *) + && let l' = Array.to_list args @ l in let l'' = try Some (expand_and_check_vars env l') with Exit -> None in match l'' with | Some l -> let deps = if occur_meta_or_existential t then + (* Probably no restrictions on allowed vars in presence of evars *) l else + (* Probably strong restrictions coming from t being evar-closed *) let fv_rels = free_rels t in let fv_ids = global_vars env t in List.filter (fun c -> @@ -1030,10 +1013,6 @@ let is_unification_pattern_evar env (_,args) l t = list_distinct deps | None -> false -(* - Pp.ppnl (prlist_with_sep spc (fun c -> match kind_of_term c with Rel _ | Var _ -> print_constr c | _ -> str "..") l'); Pp.flush_all (); -*) - let is_unification_pattern (env,nb) f l t = match kind_of_term f with | Meta _ -> diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index 685eaba3f..a35b6ffa4 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -229,9 +229,8 @@ let stdlib_use_plugins = Coq_config.has_natdynlink Order matters, for instance ground_plugin needs cc_plugins. *) let initial_plugins = - [ "Extraction_plugin"; "Jprover_plugin"; "Cc_plugin"; - "Ground_plugin"; "Dp_plugin"; "Recdef_plugin"; (*"subtac_plugin";*) - "Xml_plugin"; ] + [ "Extraction_plugin"; "Cc_plugin"; "Ground_plugin"; "Dp_plugin"; + "Recdef_plugin"; (*"subtac_plugin";*) "Xml_plugin"; ] (** Other plugins of the standard library. We need their list to avoid trying to load them if they have been statically compiled |