diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-23 18:35:09 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-23 18:35:09 +0200 |
commit | a321074cdd2f9375662c7c9f17be5c045328bd82 (patch) | |
tree | 80936ec5824dc0049d1a1f3eabc81616bd29600c | |
parent | 20d6c289bff303ec1a4cab3a56431989d0e527d2 (diff) | |
parent | 464c680b631e1ba892f2171a36002d6ca184bc4f (diff) |
Merge branch 'v8.5' into v8.6
-rw-r--r-- | doc/refman/RefMan-uti.tex | 6 | ||||
-rw-r--r-- | pretyping/unification.ml | 9 | ||||
-rw-r--r-- | test-suite/bugs/closed/5095.v | 5 |
3 files changed, 9 insertions, 11 deletions
diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex index 10271ce0c..9962ce996 100644 --- a/doc/refman/RefMan-uti.tex +++ b/doc/refman/RefMan-uti.tex @@ -102,7 +102,7 @@ generator using for instance the command: This command generates a file \texttt{Makefile} that can be used to compile all the sources of the current project. It follows the -syntax described by the output of \texttt{\% coq\_makefile ----help}. +syntax described by the output of \texttt{\% coq\_makefile -{}-help}. Once the \texttt{Makefile} file has been generated a first time, it can be used by the \texttt{make} command to compile part or all of the project. Note that once it has been generated once, as soon as @@ -112,8 +112,8 @@ automatically regenerated by an invocation of \texttt{make}. The following command generates a minimal example of \texttt{\_CoqProject} file: \begin{quotation} -\texttt{\% \{ echo '-R .} \textit{MyFancyLib} \texttt{' ; find . -name - '*.v' -print \} > \_CoqProject} +\texttt{\% ( echo "-R .\ }\textit{MyFancyLib}\texttt{" ; find .\ -name + "*.v" -print ) > \_CoqProject} \end{quotation} when executed at the root of the directory containing the project. Here the \texttt{\_CoqProject} lists all the \texttt{.v} files diff --git a/pretyping/unification.ml b/pretyping/unification.ml index bc888b897..6573bd238 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1599,14 +1599,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = let hyp = get_id d in match occurrences_of_hyp hyp occs with | NoOccurrences, InHyp -> - if indirectly_dependent c d depdecls then - (* Told explicitly not to abstract over [d], but it is dependent *) - let id' = indirect_dependency d depdecls in - errorlabstrm "" (str "Cannot abstract over " ++ Nameops.pr_id id' - ++ str " without also abstracting or erasing " ++ Nameops.pr_id hyp - ++ str ".") - else - (push_named_context_val d sign,depdecls) + (push_named_context_val d sign,depdecls) | AllOccurrences, InHyp as occ -> let occ = if likefirst then LikeFirst else AtOccs occ in let newdecl = replace_term_occ_decl_modulo occ test mkvarid d in diff --git a/test-suite/bugs/closed/5095.v b/test-suite/bugs/closed/5095.v new file mode 100644 index 000000000..b6f38e3e8 --- /dev/null +++ b/test-suite/bugs/closed/5095.v @@ -0,0 +1,5 @@ +(* Checking let-in abstraction *) +Goal let x := Set in let y := x in True. + intros x y. + (* There used to have a too strict dependency test there *) + set (s := Set) in (value of x). |