summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--.gitignore90
-rw-r--r--Makefile9
-rw-r--r--Makefile.build9
-rw-r--r--Makefile.common2
-rw-r--r--Makefile.doc2
-rw-r--r--Makefile.stage11
-rw-r--r--checker/mod_checking.ml2
-rw-r--r--config/Makefile.template3
-rwxr-xr-xconfigure25
-rw-r--r--contrib/dp/dp.ml18
-rw-r--r--contrib/extraction/common.ml10
-rw-r--r--contrib/extraction/extract_env.ml17
-rw-r--r--contrib/extraction/mlutil.ml4
-rw-r--r--contrib/funind/recdef.ml26
-rw-r--r--contrib/xml/xml.ml42
-rw-r--r--contrib/xml/xmlcommand.ml10
-rw-r--r--dev/ocamldebug-coq.template2
-rwxr-xr-xdev/v8-syntax/check-grammar18
-rw-r--r--ide/undo_lablgtk_ge212.mli3
-rwxr-xr-xinstall.sh2
-rw-r--r--interp/constrextern.ml3
-rw-r--r--interp/constrintern.ml21
-rw-r--r--kernel/indtypes.ml4
-rw-r--r--kernel/modops.ml8
-rw-r--r--lib/system.ml17
-rw-r--r--lib/system.mli4
-rw-r--r--lib/util.ml22
-rw-r--r--lib/util.mli3
-rw-r--r--library/declaremods.ml5
-rw-r--r--library/goptions.ml9
-rw-r--r--library/lib.ml28
-rw-r--r--library/library.ml12
-rw-r--r--library/states.ml5
-rw-r--r--man/coqdoc.12
-rw-r--r--parsing/g_decl_mode.ml44
-rw-r--r--parsing/g_intsyntax.ml10
-rw-r--r--parsing/g_vernac.ml44
-rw-r--r--parsing/lexer.ml425
-rw-r--r--parsing/pptactic.ml4
-rw-r--r--pretyping/cases.ml12
-rw-r--r--pretyping/clenv.ml13
-rw-r--r--pretyping/clenv.mli4
-rw-r--r--pretyping/detyping.ml5
-rw-r--r--pretyping/evarconv.ml30
-rw-r--r--pretyping/evarutil.ml77
-rw-r--r--pretyping/evarutil.mli4
-rw-r--r--pretyping/tacred.ml52
-rw-r--r--pretyping/unification.ml4
-rw-r--r--proofs/decl_mode.ml5
-rw-r--r--proofs/decl_mode.mli4
-rw-r--r--proofs/logic.ml4
-rw-r--r--scripts/coqc.ml18
-rw-r--r--scripts/coqmktop.ml4
-rw-r--r--tactics/decl_interp.ml4
-rw-r--r--tactics/decl_proof_instr.ml34
-rw-r--r--tactics/decl_proof_instr.mli13
-rw-r--r--tactics/equality.ml23
-rw-r--r--tactics/hiddentac.ml8
-rw-r--r--tactics/inv.ml4
-rw-r--r--tactics/leminv.ml6
-rw-r--r--tactics/refine.ml8
-rw-r--r--tactics/tacinterp.ml13
-rw-r--r--tactics/tactics.ml48
-rw-r--r--tactics/tauto.ml417
-rw-r--r--theories/FSets/FSetDecide.v20
-rw-r--r--theories/Init/Notations.v10
-rw-r--r--theories/Init/Tactics.v19
-rw-r--r--theories/Lists/List.v8
-rw-r--r--theories/Numbers/Rational/BigQ/BigQ.v7
-rw-r--r--theories/QArith/QArith_base.v28
-rw-r--r--theories/ZArith/Zbool.v6
-rw-r--r--theories/ZArith/Zorder.v4
-rw-r--r--tools/coq_makefile.ml48
-rw-r--r--tools/coqdep.ml44
-rw-r--r--tools/coqdoc/pretty.mll7
-rw-r--r--toplevel/metasyntax.ml24
-rw-r--r--toplevel/mltop.ml44
-rw-r--r--toplevel/toplevel.ml13
-rw-r--r--toplevel/vernacentries.ml10
79 files changed, 745 insertions, 326 deletions
diff --git a/.gitignore b/.gitignore
new file mode 100644
index 00000000..965adf7a
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,90 @@
+*.glob
+*.d
+*.d.raw
+*.vo
+*.cm*
+*.o
+*.a
+*.annot
+*.log
+*.aux
+*.dvi
+*.blg
+*.bbl
+*.idx
+*.ilg
+*.lof
+*.toc
+*.atoc
+*.comidx
+*.comind
+*.tacidx
+*.tacind
+*.erridx
+*.errind
+*.ind
+*.hcomind
+*.htacind
+*.herrind
+*.hind
+*.haux
+*.htoc
+*.v.tex
+*.v.ps
+*.v.pdf
+*.v.html
+bin
+config/Makefile
+config/coq_config.ml
+contrib/dp/dp_zenon.ml
+contrib/micromega/csdpcert
+dev/ocamldebug-coq
+dev/ocamlweb-doc/lex.ml
+dev/ocamlweb-doc/syntax.ml
+dev/ocamlweb-doc/syntax.mli
+ide/config_lexer.ml
+ide/config_parser.ml
+ide/config_parser.mli
+ide/highlight.ml
+ide/index_urls.txt
+ide/undo.mli
+ide/utf8_convert.ml
+ide/extract_index.ml
+ide/find_phrase.ml
+kernel/copcodes.ml
+kernel/byterun/coq_jumptbl.h
+scripts/tolink.ml
+states/initial.coq
+theories/Numbers/Natural/BigN/NMake.v
+tools/coqdep_lexer.ml
+tools/coqwc.ml
+tools/gallina_lexer.ml
+tools/coqdoc/pretty.ml
+tools/coqdoc/index.ml
+toplevel/mltop.byteml
+toplevel/mltop.optml
+doc/RecTutorial/RecTutorial.html
+doc/common/version.tex
+doc/faq/html
+doc/RecTutorial/RecTutorial.pdf
+doc/RecTutorial/RecTutorial.ps
+doc/refman/Reference-Manual.html
+doc/refman/Reference-Manual.sh
+doc/refman/Reference-Manual.ps
+doc/refman/Reference-Manual.pdf
+doc/refman/coqide-queries.eps
+doc/refman/coqide.eps
+doc/refman/cover.html
+doc/refman/euclid.ml
+doc/refman/euclid.mli
+doc/refman/heapsort.ml
+doc/refman/heapsort.mli
+doc/refman/html
+doc/refman/styles.hva
+doc/stdlib/Library.coqdoc.tex
+doc/stdlib/Library.out
+doc/stdlib/Library.pdf
+doc/stdlib/Library.ps
+doc/stdlib/html/
+doc/stdlib/index-list.html
+kernel/byterun/dllcoqrun.so
diff --git a/Makefile b/Makefile
index 6854de92..6873d80c 100644
--- a/Makefile
+++ b/Makefile
@@ -6,7 +6,7 @@
# # GNU Lesser General Public License Version 2.1 #
#######################################################################
-# $Id: Makefile 12063 2009-04-08 15:38:39Z herbelin $
+# $Id: Makefile 13182 2010-06-23 09:18:18Z notin $
# Makefile for Coq
@@ -24,8 +24,6 @@
# by Emacs' next-error.
###########################################################################
-export SHELL:=/bin/bash
-
export FIND_VCS_CLAUSE:='(' \
-name '{arch}' -o \
-name '.svn' -o \
@@ -183,9 +181,10 @@ docclean:
rm -f doc/*/*.ps doc/*/*.pdf
rm -rf doc/refman/html doc/stdlib/html doc/faq/html doc/tutorial/tutorial.v.html
rm -f doc/stdlib/html/*.html
- rm -f doc/refman/euclid.ml{,i} doc/refman/heapsort.ml{,i}
+ rm -f doc/refman/euclid.ml doc/refman/euclid.mli
+ rm -f doc/refman/heapsort.ml doc/refman/heapsort.mli
rm -f doc/common/version.tex
- rm -f doc/refman/*.eps doc/refman/Reference-Manual.html
+ rm -f doc/refman/styles.hva doc/refman/cover.html doc/refman/*.eps doc/refman/Reference-Manual.html
rm -f doc/coq.tex
rm -f doc/refman/styles.hva doc/refman/cover.html
diff --git a/Makefile.build b/Makefile.build
index 703c5884..148bb620 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -6,7 +6,7 @@
# # GNU Lesser General Public License Version 2.1 #
#######################################################################
-# $Id: Makefile.build 12169 2009-06-06 21:43:23Z herbelin $
+# $Id: Makefile.build 12279 2009-08-14 14:54:56Z herbelin $
# Makefile for Coq
@@ -447,6 +447,7 @@ install-ide-opt:
install-ide-files:
$(MKDIR) $(FULLIDELIB)
$(INSTALLLIB) $(IDEFILES) $(FULLIDELIB)
+ if (test -f ide/index_urls.txt); then $(INSTALLLIB) ide/index_urls.txt $(FULLIDELIB); fi
install-ide-info:
$(MKDIR) $(FULLIDELIB)
@@ -773,7 +774,7 @@ source-doc:
dev/printers.cma: $(PRINTERSCMO)
$(SHOW)'Testing $@'
- $(HIDE)$(OCAMLC) $(BYTEFLAGS) gramlib.cma $(PRINTERSCMO) -o test-printer
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) unix.cma gramlib.cma $(PRINTERSCMO) -o test-printer
@rm -f test-printer
$(SHOW)'OCAMLC -a $@'
$(HIDE)$(OCAMLC) $(BYTEFLAGS) $(PRINTERSCMO) -linkall -a -o $@
@@ -781,10 +782,10 @@ dev/printers.cma: $(PRINTERSCMO)
parsing/grammar.cma: $(GRAMMARCMO)
$(SHOW)'Testing $@'
@touch test.ml4
- $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) -I $(CAMLLIB) unix.cma $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar
@rm -f test-grammar test.*
$(SHOW)'OCAMLC -a $@'
- $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(GRAMMARCMO) -linkall -a -o $@
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) unix.cma $(GRAMMARCMO) -linkall -a -o $@
# toplevel/mltop.ml4 (ifdef Byte)
diff --git a/Makefile.common b/Makefile.common
index d6f43cf5..4d76e9e5 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -435,7 +435,7 @@ MCHECKER:=\
# grammar modules with camlp4
GRAMMARNEEDEDCMO:=\
- lib/pp_control.cmo lib/pp.cmo lib/compat.cmo lib/flags.cmo \
+ lib/profile.cmo lib/pp_control.cmo lib/pp.cmo lib/compat.cmo lib/flags.cmo \
lib/util.cmo lib/bigint.cmo lib/dyn.cmo lib/hashcons.cmo lib/predicate.cmo \
lib/rtree.cmo lib/option.cmo \
kernel/names.cmo kernel/univ.cmo \
diff --git a/Makefile.doc b/Makefile.doc
index 795e0e5c..f481d681 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -209,7 +209,7 @@ else
doc/stdlib/Library.coqdoc.tex: | $(COQDOC) $(THEORIESLIGHTVO)
endif
$(COQDOC) -q -boot --gallina --body-only --latex --stdout \
- -R theories Coq $(THEORIESLIGHTVO:.vo=.v) >> $@
+ -R theories Coq $(THEORIESLIGHTVO:.vo=.v) > $@
doc/stdlib/Library.dvi: $(DOCCOMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Library.tex
(cd doc/stdlib;\
diff --git a/Makefile.stage1 b/Makefile.stage1
index c39a6372..a60d388f 100644
--- a/Makefile.stage1
+++ b/Makefile.stage1
@@ -6,7 +6,6 @@
# # GNU Lesser General Public License Version 2.1 #
#######################################################################
-export SHELL:=/bin/bash
include Makefile.build
# All includes must be declared secondary, otherwise make will delete
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 9e7a2336..24000591 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -306,7 +306,7 @@ and check_structure_field (s,env) mp lab = function
let sub = join_alias sub (map_mp mp' mp2') in
let sub = add_mp mp' mp2' sub in
(join s sub, register_alias mp' mp2 env)
- with Not_found -> failwith "unkown aliased module")
+ with Not_found -> failwith "unknown aliased module")
| SFBmodtype mty ->
let kn = MPdot(mp, lab) in
check_module_type env mty;
diff --git a/config/Makefile.template b/config/Makefile.template
index 6f9fac3c..4d45f1b4 100644
--- a/config/Makefile.template
+++ b/config/Makefile.template
@@ -49,6 +49,9 @@ CAMLP4BIN="CAMLP4BINDIRECTORY"
# Ocaml version number
CAMLVERSION=CAMLTAG
+# Ocaml libraries
+CAMLLIB="CAMLLIBDIRECTORY"
+
# Ocaml .h directory
CAMLHLIB="CAMLLIBDIRECTORY"
diff --git a/configure b/configure
index 1ba4eaba..db7a55a0 100755
--- a/configure
+++ b/configure
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/bin/sh
##################################
#
@@ -6,7 +6,7 @@
#
##################################
-VERSION=8.2pl1
+VERSION=8.2pl2
VOMAGIC=08200
STATEMAGIC=58200
DATE=`LANG=C date +"%B %Y"`
@@ -331,7 +331,7 @@ if [ "$MAKE" != "" ]; then
OK="no"
if [ -x ./make ]; then
MAKEVERSION=`./make -v | head -1`
- if [ "$MAKEVERSION" == "GNU Make 3.81" ]; then OK="yes"; fi
+ if [ "$MAKEVERSION" = "GNU Make 3.81" ]; then OK="yes"; fi
fi
if [ $OK = "no" ]; then
echo "GNU Make >= 3.81 is needed"
@@ -363,7 +363,7 @@ if [ "$browser_spec" = "no" ]; then
fi
if [ "$wwwcoq_spec" = "no" ]; then
- WWWCOQ="http://www.lix.polytechnique.fr/coq/"
+ WWWCOQ="http://coq.inria.fr/"
fi
#########################################
@@ -665,17 +665,14 @@ esac
if test "$with_doc" = "all"
then
- if test "`which latex`" = ""
- then
- echo "latex was not found; documentation will not be available"
- with_doc=no
- else
- if test "`which hevea`" = ""
- then
+ for cmd in "latex" "hevea" "pngtopnm" "pnmtops" ; do
+ if test ! -x "`which $cmd`"
+ then
+ echo "$cmd was not found; documentation will not be available"
with_doc=no
- echo "hevea was not found: documentation will not be available"
+ break
fi
- fi
+ done
fi
###########################################
@@ -1080,4 +1077,4 @@ echo
echo "*Warning* To compile the system for a new architecture"
echo " don't forget to do a 'make archclean' before './configure'."
-# $Id: configure 12219 2009-07-01 09:58:00Z notin $
+# $Id: configure 13223 2010-06-29 18:28:35Z notin $
diff --git a/contrib/dp/dp.ml b/contrib/dp/dp.ml
index 79ffaf3f..d8803847 100644
--- a/contrib/dp/dp.ml
+++ b/contrib/dp/dp.ml
@@ -701,7 +701,7 @@ let file_contents f =
let timeout_sys_command cmd =
if !debug then Format.eprintf "command line: %s@." cmd;
let out = Filename.temp_file "out" "" in
- let cmd = sprintf "cpulimit %d %s > %s 2>&1" !timeout cmd out in
+ let cmd = sprintf "why-cpulimit %d %s > %s 2>&1" !timeout cmd out in
let ret = Sys.command cmd in
if !debug then
Format.eprintf "Output file %s:@.%s@." out (file_contents out);
@@ -731,12 +731,12 @@ let why_files f = String.concat " " (!prelude_files @ [f])
let call_simplify fwhy =
let cmd =
- sprintf "why --no-arrays --simplify --encoding sstrat %s" (why_files fwhy)
+ sprintf "why --simplify %s" (why_files fwhy)
in
if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
let fsx = Filename.chop_suffix fwhy ".why" ^ "_why.sx" in
let cmd =
- sprintf "timeout %d Simplify %s > out 2>&1 && grep -q -w Valid out"
+ sprintf "why-cpulimit %d Simplify %s > out 2>&1 && grep -q -w Valid out"
!timeout fsx
in
let out = Sys.command cmd in
@@ -747,7 +747,7 @@ let call_simplify fwhy =
r
let call_ergo fwhy =
- let cmd = sprintf "why --no-arrays --why %s" (why_files fwhy) in
+ let cmd = sprintf "why --alt-ergo %s" (why_files fwhy) in
if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
let fwhy = Filename.chop_suffix fwhy ".why" ^ "_why.why" in
let ftrace = Filename.temp_file "ergo_trace" "" in
@@ -797,12 +797,12 @@ let call_zenon fwhy =
let call_yices fwhy =
let cmd =
- sprintf "why --no-arrays -smtlib --encoding sstrat %s" (why_files fwhy)
+ sprintf "why -smtlib --encoding sstrat %s" (why_files fwhy)
in
if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
let fsmt = Filename.chop_suffix fwhy ".why" ^ "_why.smt" in
let cmd =
- sprintf "timeout %d yices -pc 0 -smt < %s > out 2>&1 && grep -q -w unsat out"
+ sprintf "why-cpulimit %d yices -pc 0 -smt %s > out 2>&1 && grep -q -w unsat out"
!timeout fsmt
in
let out = Sys.command cmd in
@@ -814,7 +814,7 @@ let call_yices fwhy =
let call_cvcl fwhy =
let cmd =
- sprintf "why --no-arrays --cvcl --encoding sstrat %s" (why_files fwhy)
+ sprintf "why --cvcl --encoding sstrat %s" (why_files fwhy)
in
if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
let fcvc = Filename.chop_suffix fwhy ".why" ^ "_why.cvc" in
@@ -831,7 +831,7 @@ let call_cvcl fwhy =
let call_harvey fwhy =
let cmd =
- sprintf "why --no-arrays --harvey --encoding strat %s" (why_files fwhy)
+ sprintf "why --harvey --encoding strat %s" (why_files fwhy)
in
if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
let frv = Filename.chop_suffix fwhy ".why" ^ "_why.rv" in
@@ -856,7 +856,7 @@ let call_harvey fwhy =
r
let call_gwhy fwhy =
- let cmd = sprintf "gwhy --no-arrays %s" (why_files fwhy) in
+ let cmd = sprintf "gwhy %s" (why_files fwhy) in
if Sys.command cmd <> 0 then ignore (Sys.command (sprintf "emacs %s" fwhy));
NoAnswer
diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 02173c1f..73f44e68 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: common.ml 11559 2008-11-07 22:03:34Z letouzey $ i*)
+(*i $Id: common.ml 13200 2010-06-25 22:36:25Z letouzey $ i*)
open Pp
open Util
@@ -21,6 +21,8 @@ open Mlutil
open Modutil
open Mod_subst
+let string_of_id id = ascii_of_ident (Names.string_of_id id)
+
(*s Some pretty-print utility functions. *)
let pp_par par st = if par then str "(" ++ st ++ str ")" else st
@@ -73,7 +75,11 @@ let is_upper s = match s.[0] with 'A' .. 'Z' -> true | _ -> false
let is_lower s = match s.[0] with 'a' .. 'z' | '_' -> true | _ -> false
let lowercase_id id = id_of_string (String.uncapitalize (string_of_id id))
-let uppercase_id id = id_of_string (String.capitalize (string_of_id id))
+let uppercase_id id =
+ let s = string_of_id id in
+ assert (s<>"");
+ if s.[0] = '_' then id_of_string ("Coq_"^s)
+ else id_of_string (String.capitalize s)
type kind = Term | Type | Cons | Mod
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 49a86200..057a7b29 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: extract_env.ml 11846 2009-01-22 18:55:10Z letouzey $ i*)
+(*i $Id: extract_env.ml 13201 2010-06-25 22:36:27Z letouzey $ i*)
open Term
open Declarations
@@ -489,15 +489,12 @@ let simple_extraction r = match locate_ref [r] with
| ([], [mp]) as p -> full_extr None p
| [r],[] ->
init false;
- if is_custom r then
- msgnl (str "User defined extraction:" ++ spc () ++
- str (find_custom r) ++ fnl ())
- else
- let struc = optimize_struct [r] (mono_environment [r] []) in
- let d = get_decl_in_structure r struc in
- warning_axioms ();
- print_one_decl struc (modpath_of_r r) d;
- reset ()
+ let struc = optimize_struct [r] (mono_environment [r] []) in
+ let d = get_decl_in_structure r struc in
+ warning_axioms ();
+ if is_custom r then msgnl (str "(** User defined extraction *)");
+ print_one_decl struc (modpath_of_r r) d;
+ reset ()
| _ -> assert false
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 79aeea33..4e2904ba 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: mlutil.ml 10329 2007-11-21 21:21:36Z letouzey $ i*)
+(*i $Id: mlutil.ml 13202 2010-06-25 22:36:30Z letouzey $ i*)
(*i*)
open Pp
@@ -578,7 +578,7 @@ let eta_red e =
if m = n then
[], f, a
else if m < n then
- snd (list_chop (n-m) ids), f, a
+ list_skipn m ids, f, a
else (* m > n *)
let a1,a2 = list_chop (m-n) a in
[], MLapp (f,a1), a2
diff --git a/contrib/funind/recdef.ml b/contrib/funind/recdef.ml
index 6dc0d5bf..14bf7cf8 100644
--- a/contrib/funind/recdef.ml
+++ b/contrib/funind/recdef.ml
@@ -8,7 +8,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: recdef.ml 11671 2008-12-12 12:43:03Z herbelin $ *)
+(* $Id: recdef.ml 12221 2009-07-04 21:53:12Z jforest $ *)
open Term
open Termops
@@ -960,11 +960,6 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
let ids' = pf_ids_of_hyps g in
lid := List.rev (list_subtract ids' ids);
if !lid = [] then lid := [hid];
-(* list_iter_i *)
-(* (fun i v -> *)
-(* msgnl (str "hyp" ++ int i ++ str " " ++ *)
-(* Nameops.pr_id v ++ fnl () ++ fnl())) *)
-(* !lid; *)
tclIDTAC g
)
g
@@ -976,9 +971,22 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
Auto.h_auto None [] (Some []) g
| _ ->
incr h_num;
- tclTHEN
- (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings))
- e_assumption
+ (observe_tac "finishing using"
+ (
+ tclCOMPLETE(
+ tclFIRST[
+ tclTHEN
+ (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings))
+ e_assumption;
+ Eauto.eauto_with_bases
+ false
+ (true,5)
+ [delayed_force refl_equal]
+ [Auto.Hint_db.empty empty_transparent_state false]
+ ]
+ )
+ )
+ )
g)
;
Command.save_named opacity;
diff --git a/contrib/xml/xml.ml4 b/contrib/xml/xml.ml4
index e2d04cb7..5b217119 100644
--- a/contrib/xml/xml.ml4
+++ b/contrib/xml/xml.ml4
@@ -70,7 +70,7 @@ let pp strm fn =
let ch = open_out filename in
pp_ch strm ch;
close_out ch ;
- print_string ("\nWriting on file \"" ^ filename ^ "\" was succesful\n");
+ print_string ("\nWriting on file \"" ^ filename ^ "\" was successful\n");
flush stdout
| None ->
pp_ch strm stdout
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 1ae18661..f4719594 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -662,21 +662,21 @@ let _ =
| Some fn ->
let ch = open_out (fn ^ ".v") in
Buffer.output_buffer ch theory_buffer ;
+ close_out ch;
+ (* dummy glob file *)
+ let ch = open_out (fn ^ ".glob") in
close_out ch
end ;
Option.iter
(fun fn ->
let coqdoc = Filename.concat (Envars.coqbin ()) ("coqdoc" ^ Coq_config.exec_extension) in
let options = " --html -s --body-only --no-index --latin1 --raw-comments" in
- let dir = Option.get xml_library_root in
let command cmd =
if Sys.command cmd <> 0 then
Util.anomaly ("Error executing \"" ^ cmd ^ "\"")
in
- command (coqdoc^options^" -d "^dir^" "^fn^".v");
- let dot = if fn.[0]='/' then "." else "" in
- command ("mv "^dir^"/"^dot^"*.html "^fn^".xml ");
- command ("rm "^fn^".v");
+ command (coqdoc^options^" -o "^fn^".xml "^fn^".v");
+ command ("rm "^fn^".v "^fn^".glob");
print_string("\nWriting on file \"" ^ fn ^ ".xml\" was successful\n"))
ofn)
;;
diff --git a/dev/ocamldebug-coq.template b/dev/ocamldebug-coq.template
index 560d06d9..5f49561b 100644
--- a/dev/ocamldebug-coq.template
+++ b/dev/ocamldebug-coq.template
@@ -19,7 +19,7 @@ exec $OCAMLDEBUG \
-I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config \
-I $COQTOP/contrib/extraction -I $COQTOP/contrib/field \
-I $COQTOP/contrib/fourier -I $COQTOP/contrib/firstorder \
- -I $COQTOP/contrib/interface \
+ -I $COQTOP/contrib/interface -I $COQTOP/contrib/cc \
-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/v8-syntax/check-grammar b/dev/v8-syntax/check-grammar
index 67da1bc5..194a55fe 100755
--- a/dev/v8-syntax/check-grammar
+++ b/dev/v8-syntax/check-grammar
@@ -1,31 +1,31 @@
-#!/bin/bash
+#!/bin/sh
# This scripts checks that the new grammar of Coq as defined in syntax-v8.tex
# is consistent in the sense that all invoked non-terminals are defined
-defined-nt() {
+defined_nt() {
grep "\\DEFNT{.*}" syntax-v8.tex | sed -e "s|.*DEFNT{\([^}]*\)}.*|\1|"|\
sort | sort -u
}
-used-nt() {
+used_nt() {
cat syntax-v8.tex | tr \\\\ \\n | grep "^NT{.*}" |\
sed -e "s|^NT{\([^}]*\)}.*|\1|" | egrep -v ^\#1\|non-terminal | sort -u
}
-used-term() {
+used_term() {
cat syntax-v8.tex | tr \\\\ \\n | grep "^TERM{.*}" |\
sed -e "s|^TERM{\([^}]*\)}.*|\1|" -e "s|\\$||g" | egrep -v ^\#1\|terminal | sort -u
}
-used-kwd() {
+used_kwd() {
cat syntax-v8.tex | tr \\\\ \\n | grep "^KWD{.*}" |\
sed -e "s|^KWD{\([^}]*\)}.*|\1|" -e "s|\\$||g" | egrep -v ^\#1 | sort -u
}
-defined-nt > def
-used-nt > use
-used-term > use-t
-used-kwd > use-k
+defined_nt > def
+used_nt > use
+used_term > use-t
+used_kwd > use-k
diff def use > df
###############################
diff --git a/ide/undo_lablgtk_ge212.mli b/ide/undo_lablgtk_ge212.mli
index 916a06e9..4488b5e9 100644
--- a/ide/undo_lablgtk_ge212.mli
+++ b/ide/undo_lablgtk_ge212.mli
@@ -10,9 +10,10 @@
(* An undoable view class *)
-class undoable_view : [> Gtk.text_view] Gtk.obj ->
+class undoable_view : ([> Gtk.text_view] as 'a) Gtk.obj ->
object
inherit GText.view
+ val obj : 'a Gtk.obj
method undo : bool
method redo : bool
method clear_undo : unit
diff --git a/install.sh b/install.sh
index c2f8215b..277222f5 100755
--- a/install.sh
+++ b/install.sh
@@ -1,4 +1,4 @@
-#! /bin/bash
+#! /bin/sh
dest="$1"
shift
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index f99af68e..99bcf159 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: constrextern.ml 11576 2008-11-10 19:13:15Z msozeau $ *)
+(* $Id: constrextern.ml 12495 2009-11-11 12:10:44Z herbelin $ *)
(*i*)
open Pp
@@ -363,7 +363,6 @@ let bind_env (sigma,sigmalist as fullsigma) var v =
let rec match_cases_pattern metas sigma a1 a2 = match (a1,a2) with
| r1, AVar id2 when List.mem id2 metas -> bind_env sigma id2 r1
| PatVar (_,Anonymous), AHole _ -> sigma
- | a, AHole _ -> sigma
| PatCstr (loc,(ind,_ as r1),args1,_), _ ->
let nparams =
(fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 8d6a92a2..c8faf911 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: constrintern.ml 11739 2009-01-02 19:33:19Z herbelin $ *)
+(* $Id: constrintern.ml 13131 2010-06-13 18:45:17Z herbelin $ *)
open Pp
open Util
@@ -450,8 +450,8 @@ let rec simple_adjust_scopes n = function
let find_remaining_constructor_scopes pl1 pl2 (ind,j as cstr) =
let (mib,mip) = Inductive.lookup_mind_specif (Global.env()) ind in
let npar = mib.Declarations.mind_nparams in
- snd (list_chop (List.length pl1 + npar)
- (simple_adjust_scopes (npar + List.length pl2)
+ snd (list_chop (npar + List.length pl1)
+ (simple_adjust_scopes (npar + List.length pl1 + List.length pl2)
(find_arguments_scope (ConstructRef cstr))))
(**********************************************************************)
@@ -526,6 +526,7 @@ let error_invalid_pattern_notation loc =
let chop_aconstr_constructor loc (ind,k) args =
let nparams = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
+ if nparams > List.length args then error_invalid_pattern_notation loc;
let params,args = list_chop nparams args in
List.iter (function AHole _ -> ()
| _ -> error_invalid_pattern_notation loc) params;
@@ -728,8 +729,7 @@ let locate_if_isevar loc na = function
let check_hidden_implicit_parameters id (_,_,_,(indnames,_)) =
if List.mem id indnames then
errorlabstrm "" (strbrk "A parameter or name of an inductive type " ++
- pr_id id ++ strbrk " must not be used as a bound variable in the type \
-of its constructor.")
+ pr_id id ++ strbrk " is not allowed to be used as a bound variable in the type of its constructor.")
let push_name_env ?(fail_anonymous=false) lvar (ids,unb,tmpsc,scopes as env) = function
| Anonymous ->
@@ -1060,15 +1060,17 @@ let internalise sigma globalenv env allow_patvar lvar c =
| CLetTuple (loc, nal, (na,po), b, c) ->
let env' = reset_tmp_scope env in
let ((b',(na',_)),ids) = intern_case_item env' (b,(na,None)) in
- let env'' = List.fold_left (push_name_env lvar) env ids in
- let p' = Option.map (intern_type env'') po in
+ let p' = Option.map (fun p ->
+ let env'' = List.fold_left (push_name_env lvar) env ids in
+ intern_type env'' p) po in
RLetTuple (loc, nal, (na', p'), b',
intern (List.fold_left (push_name_env lvar) env nal) c)
| CIf (loc, c, (na,po), b1, b2) ->
let env' = reset_tmp_scope env in
let ((c',(na',_)),ids) = intern_case_item env' (c,(na,None)) in
- let env'' = List.fold_left (push_name_env lvar) env ids in
- let p' = Option.map (intern_type env'') po in
+ let p' = Option.map (fun p ->
+ let env'' = List.fold_left (push_name_env lvar) env ids in
+ intern_type env'' p) po in
RIf (loc, c', (na', p'), intern env b1, intern env b2)
| CHole (loc, k) ->
RHole (loc, match k with Some k -> k | None -> Evd.QuestionMark (Evd.Define true))
@@ -1147,6 +1149,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
[], None in
let na = match tm', na with
| RVar (_,id), None when Idset.mem id vars -> Name id
+ | RRef (loc, VarRef id), None -> Name id
| _, None -> Anonymous
| _, Some na -> na in
(tm',(na,typ)), na::ids
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 06764834..941ab046 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: indtypes.ml 11784 2009-01-14 11:36:32Z herbelin $ *)
+(* $Id: indtypes.ml 12616 2009-12-30 15:02:26Z herbelin $ *)
open Util
open Names
@@ -494,7 +494,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps i nargs lcnames indlc =
raise (IllFormedInd LocalNotConstructor)
else
if not (List.for_all (noccur_between n ntypes) largs)
- then raise (IllFormedInd (LocalNonPos n));
+ then failwith_non_pos_list n ntypes largs;
(nmr,List.rev lrec)
in check_constr_rec ienv nmr [] c
in
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 949a7402..34d9e930 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: modops.ml 11923 2009-02-13 12:20:27Z soubiran $ i*)
+(*i $Id: modops.ml 12234 2009-07-09 09:14:09Z soubiran $ i*)
(*i*)
open Util
@@ -143,11 +143,13 @@ let rec subst_with_body sub = function
and subst_modtype sub mtb =
let typ_expr' = subst_struct_expr sub mtb.typ_expr in
- if typ_expr'==mtb.typ_expr then
+ let sub_mtb = join_alias mtb.typ_alias sub in
+ if typ_expr'==mtb.typ_expr && sub_mtb==mtb.typ_alias then
mtb
else
{ mtb with
- typ_expr = typ_expr'}
+ typ_expr = typ_expr';
+ typ_alias = sub_mtb}
and subst_structure sub sign =
let subst_body = function
diff --git a/lib/system.ml b/lib/system.ml
index 65826c81..3fa32ef8 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: system.ml 11801 2009-01-18 20:11:41Z herbelin $ *)
+(* $Id: system.ml 13175 2010-06-22 06:28:37Z herbelin $ *)
open Pp
open Util
@@ -153,8 +153,12 @@ let where_in_path ?(warn=true) path filename =
let find_file_in_path ?(warn=true) paths filename =
if not (Filename.is_implicit filename) then
- let root = Filename.dirname filename in
- root, filename
+ if Sys.file_exists filename then
+ let root = Filename.dirname filename in
+ root, filename
+ else
+ errorlabstrm "System.find_file_in_path"
+ (hov 0 (str "Can't find file" ++ spc () ++ str filename))
else
try where_in_path ~warn paths filename
with Not_found ->
@@ -224,6 +228,13 @@ let extern_intern ?(warn=true) magic suffix =
in
(extern_state,intern_state)
+let with_magic_number_check f a =
+ try f a
+ with Bad_magic_number fname ->
+ errorlabstrm "with_magic_number_check"
+ (str"File " ++ str fname ++ strbrk" has bad magic number." ++ spc () ++
+ strbrk "It is corrupted or was compiled with another version of Coq.")
+
(* Communication through files with another executable *)
let connect writefun readfun com =
diff --git a/lib/system.mli b/lib/system.mli
index ba5aa408..426a00df 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: system.mli 11801 2009-01-18 20:11:41Z herbelin $ i*)
+(*i $Id: system.mli 13175 2010-06-22 06:28:37Z herbelin $ i*)
(*s Files and load paths. Load path entries remember the original root
given by the user. For efficiency, we keep the full path (field
@@ -54,6 +54,8 @@ val raw_extern_intern : int -> string ->
val extern_intern : ?warn:bool -> int -> string ->
(string -> 'a -> unit) * (load_path -> string -> 'a)
+val with_magic_number_check : ('a -> 'b) -> 'a -> 'b
+
(*s Sending/receiving once with external executable *)
val connect : (out_channel -> unit) -> (in_channel -> 'a) -> string -> 'a
diff --git a/lib/util.ml b/lib/util.ml
index dce36419..0d6e7ff2 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id: util.ml 12181 2009-06-10 20:53:09Z glondu $ *)
+(* $Id: util.ml 13200 2010-06-25 22:36:25Z letouzey $ *)
open Pp
@@ -486,6 +486,26 @@ let lowercase_first_char_utf8 s =
let j, n = next_utf8 s 0 in
utf8_of_unicode (lowercase_unicode (String.sub s 0 j) n)
+(* For extraction, we need to encode unicode character into ascii ones *)
+
+let ascii_of_ident s =
+ let check_ascii s =
+ let ok = ref true in
+ String.iter (fun c -> if Char.code c >= 128 then ok := false) s;
+ !ok
+ in
+ if check_ascii s then s else
+ let i = ref 0 and out = ref "" in
+ begin try while true do
+ let j, n = next_utf8 s !i in
+ out :=
+ if n >= 128
+ then Printf.sprintf "%s__U%04x_" !out n
+ else Printf.sprintf "%s%c" !out s.[!i];
+ i := !i + j
+ done with End_of_input -> () end;
+ !out
+
(* Lists *)
let list_intersect l1 l2 =
diff --git a/lib/util.mli b/lib/util.mli
index 5432eb98..97bda074 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(*i $Id: util.mli 11897 2009-02-09 19:28:02Z barras $ i*)
+(*i $Id: util.mli 13200 2010-06-25 22:36:25Z letouzey $ i*)
(*i*)
open Pp
@@ -94,6 +94,7 @@ val classify_unicode : int -> utf8_status
val check_ident : string -> unit
val check_ident_soft : string -> unit
val lowercase_first_char_utf8 : string -> string
+val ascii_of_ident : string -> string
(*s Lists. *)
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 93021384..cfada00c 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: declaremods.ml 12204 2009-06-22 16:06:49Z soubiran $ i*)
+(*i $Id: declaremods.ml 12295 2009-08-27 11:01:49Z soubiran $ i*)
open Pp
open Util
open Names
@@ -851,8 +851,7 @@ let classify_import (_,(export,_ as obj)) =
if export then Substitute obj else Dispose
let subst_import (_,subst,(export,mp as obj)) =
- let subst' = remove_alias subst in
- let mp' = subst_mp subst' mp in
+ let mp' = subst_mp subst mp in
if mp'==mp then obj else
(export,mp')
diff --git a/library/goptions.ml b/library/goptions.ml
index a9b33235..8625ee52 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: goptions.ml 10348 2007-12-06 17:36:14Z aspiwack $ *)
+(* $Id: goptions.ml 13196 2010-06-25 18:01:50Z herbelin $ *)
(* This module manages customization parameters at the vernacular level *)
@@ -297,10 +297,11 @@ let set_int_option_value = set_option_value
(fun v -> function
| (IntValue _) -> IntValue v
| _ -> bad_type_error ())
-let set_bool_option_value = set_option_value
- (fun v -> function
+let set_bool_option_value key v =
+ try set_option_value (fun v -> function
| (BoolValue _) -> BoolValue v
- | _ -> bad_type_error ())
+ | _ -> bad_type_error ()) key v
+ with UserError (_,s) -> Flags.if_verbose msg_warning s
let set_string_option_value = set_option_value
(fun v -> function
| (StringValue _) -> StringValue v
diff --git a/library/lib.ml b/library/lib.ml
index 4a124cec..f0ec488b 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: lib.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
+(* $Id: lib.ml 12496 2009-11-11 13:37:57Z herbelin $ *)
open Pp
open Util
@@ -171,9 +171,8 @@ let find_split_p p =
let split_lib_gen test =
let rec collect after equal = function
- | hd::strict_before as before ->
- if test hd then collect after (hd::equal) strict_before else after,equal,before
- | [] as before -> after,equal,before
+ | hd::before when test hd -> collect after (hd::equal) before
+ | before -> after,equal,before
in
let rec findeq after = function
| hd :: before ->
@@ -194,7 +193,14 @@ let split_lib_gen test =
| None -> error "no such entry"
| Some r -> r
-let split_lib sp = split_lib_gen (fun x -> (fst x) = sp)
+let split_lib sp = split_lib_gen (fun x -> fst x = sp)
+
+let split_lib_at_opening sp =
+ split_lib_gen (function
+ | x,(OpenedSection _|OpenedModule _|OpenedModtype _|CompilingLibrary _) ->
+ x = sp
+ | _ ->
+ false)
(* Adding operations. *)
@@ -299,7 +305,7 @@ let end_module id =
with Not_found ->
error "no opened modules"
in
- let (after,modopening,before) = split_lib oname in
+ let (after,modopening,before) = split_lib_at_opening oname in
lib_stk := before;
add_entry (make_oname id) (ClosedModule (List.rev_append after (List.rev modopening)));
let prefix = !path_prefix in
@@ -344,7 +350,7 @@ let end_modtype id =
with Not_found ->
error "no opened module types"
in
- let (after,modtypeopening,before) = split_lib sp in
+ let (after,modtypeopening,before) = split_lib_at_opening sp in
lib_stk := before;
add_entry (make_oname id) (ClosedModtype (List.rev_append after (List.rev modtypeopening)));
let dir = !path_prefix in
@@ -407,7 +413,7 @@ let end_compilation dir =
("The current open module has name "^ (Names.string_of_dirpath m) ^
" and not " ^ (Names.string_of_dirpath m));
in
- let (after,_,before) = split_lib oname in
+ let (after,_,before) = split_lib_at_opening oname in
comp_name := None;
!path_prefix,after
@@ -587,7 +593,7 @@ let close_section id =
with Not_found ->
error "No opened section."
in
- let (secdecls,secopening,before) = split_lib oname in
+ let (secdecls,secopening,before) = split_lib_at_opening oname in
lib_stk := before;
let full_olddir = fst !path_prefix in
pop_path_prefix ();
@@ -640,7 +646,7 @@ let reset_to_gen test =
let (_,_,before) = split_lib_gen test in
set_lib_stk before
-let reset_to sp = reset_to_gen (fun x -> (fst x) = sp)
+let reset_to sp = reset_to_gen (fun x -> fst x = sp)
let reset_to_state sp =
let (_,eq,before) = split_lib sp in
@@ -667,7 +673,7 @@ let delete_gen test =
in
set_lib_stk (List.rev_append (chop_at_dot after) (chop_before_dot before))
-let delete sp = delete_gen (fun x -> (fst x) = sp)
+let delete sp = delete_gen (fun x -> fst x = sp)
let reset_name (loc,id) =
let (sp,_) =
diff --git a/library/library.ml b/library/library.ml
index 0e1342f0..2c6d02ae 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: library.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: library.ml 13175 2010-06-22 06:28:37Z herbelin $ *)
open Pp
open Util
@@ -328,14 +328,6 @@ let (in_import, out_import) =
let (raw_extern_library, raw_intern_library) =
System.raw_extern_intern Coq_config.vo_magic_number ".vo"
-let with_magic_number_check f a =
- try f a
- with System.Bad_magic_number fname ->
- errorlabstrm "with_magic_number_check"
- (str"File " ++ str fname ++ spc () ++ str"has bad magic number." ++
- spc () ++ str"It is corrupted" ++ spc () ++
- str"or was compiled with another version of Coq.")
-
(************************************************************************)
(*s Locate absolute or partially qualified library names in the path *)
@@ -414,7 +406,7 @@ let mk_library md digest = {
library_digest = digest }
let intern_from_file f =
- let ch = with_magic_number_check raw_intern_library f in
+ let ch = System.with_magic_number_check raw_intern_library f in
let md = System.marshal_in ch in
let digest = System.marshal_in ch in
close_in ch;
diff --git a/library/states.ml b/library/states.ml
index c81f9614..3a4be1ca 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: states.ml 12080 2009-04-11 16:56:20Z herbelin $ *)
+(* $Id: states.ml 13175 2010-06-22 06:28:37Z herbelin $ *)
open System
@@ -24,7 +24,8 @@ let (extern_state,intern_state) =
extern_intern Coq_config.state_magic_number ".coq" in
(fun s -> raw_extern s (freeze())),
(fun s ->
- unfreeze (raw_intern (Library.get_load_paths ()) s);
+ unfreeze
+ (with_magic_number_check (raw_intern (Library.get_load_paths ())) s);
Library.overwrite_library_filenames s)
(* Rollback. *)
diff --git a/man/coqdoc.1 b/man/coqdoc.1
index 45fcafd2..e07ccdd3 100644
--- a/man/coqdoc.1
+++ b/man/coqdoc.1
@@ -75,7 +75,7 @@ Considers the file `file' respectively as a .v (or .g) file or a .tex file.
.TP
.BI \-\-files\-from \ file
Read file names to process in file `file' as if they were given on the
-command line. Useful for program sources splitted in several
+command line. Useful for program sources split in several
directories.
.TP
.B \-q, \ \-\-quiet
diff --git a/parsing/g_decl_mode.ml4 b/parsing/g_decl_mode.ml4
index 61c3474d..35fc064b 100644
--- a/parsing/g_decl_mode.ml4
+++ b/parsing/g_decl_mode.ml4
@@ -9,7 +9,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
(*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*)
-(* $Id: g_decl_mode.ml4 10739 2008-04-01 14:45:20Z herbelin $ *)
+(* $Id: g_decl_mode.ml4 12414 2009-10-25 18:50:41Z corbinea $ *)
open Decl_expr
@@ -220,7 +220,7 @@ GLOBAL: proof_instr;
intro_step:
[[ IDENT "suppose" ; h=assume_clause -> Psuppose h
| IDENT "suppose" ; IDENT "it"; IDENT "is" ; c=pattern LEVEL "0" ;
- po=OPT[ IDENT "with"; p=LIST1 hyp -> p ] ;
+ po=OPT[ "with"; p=LIST1 hyp SEP ","-> p ] ;
ho=OPT[ IDENT "and" ; h=suppose_clause -> h ] ->
Pcase (none_is_empty po,c,none_is_empty ho)
| "let" ; v=let_vars -> Plet v
diff --git a/parsing/g_intsyntax.ml b/parsing/g_intsyntax.ml
index a589ccf1..64fa0b49 100644
--- a/parsing/g_intsyntax.ml
+++ b/parsing/g_intsyntax.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: g_intsyntax.ml 11309 2008-08-06 10:30:35Z herbelin $ i*)
+(*i $Id: g_intsyntax.ml 12509 2009-11-12 15:52:50Z letouzey $ i*)
(* digit-based syntax for int31, bigN bigZ and bigQ *)
@@ -92,13 +92,15 @@ let bigZ_neg = ConstructRef ((bigZ_id "t_",0),2)
(*bigQ stuff*)
let bigQ_module = ["Coq"; "Numbers"; "Rational"; "BigQ"; "BigQ"]
-let qmake_module = ["Coq"; "Numbers"; "Rational"; "BigQ"; "QMake_base"]
+let qmake_module = ["Coq"; "Numbers"; "Rational"; "BigQ"; "QMake"]
let bigQ_path = make_path (bigQ_module@["BigQ"]) "t"
(* big ugly hack bis *)
-let bigQ_id = make_kn qmake_module
+let bigQ_id id = (Obj.magic ((Names.MPdot ((Names.MPfile (make_dir bigQ_module)),
+ Names.mk_label "BigQ")),
+ [], Names.id_of_string id) : Names.kernel_name)
let bigQ_scope = "bigQ_scope"
-let bigQ_z = ConstructRef ((bigQ_id "q_type",0),1)
+let bigQ_z = ConstructRef ((bigQ_id "t_",0),1)
(*** Definition of the Non_closed exception, used in the pretty printing ***)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index b2d67e1c..f727dfea 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -9,7 +9,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
(*i camlp4use: "pa_extend.cmo" i*)
-(* $Id: g_vernac.ml4 12187 2009-06-13 19:36:59Z msozeau $ *)
+(* $Id: g_vernac.ml4 13197 2010-06-25 22:36:17Z letouzey $ *)
open Pp
@@ -663,6 +663,8 @@ GEXTEND Gram
check_command: (* TODO: rapprocher Eval et Check *)
[ [ IDENT "Eval"; r = Tactic.red_expr; "in"; c = lconstr ->
fun g -> VernacCheckMayEval (Some r, g, c)
+ | IDENT "Compute"; c = lconstr ->
+ fun g -> VernacCheckMayEval (Some Rawterm.CbvVm, g, c)
| IDENT "Check"; c = lconstr ->
fun g -> VernacCheckMayEval (None, g, c) ] ]
;
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 2633386f..52b5ede7 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: lexer.ml4 11786 2009-01-14 13:07:34Z herbelin $ i*)
+(*i $Id: lexer.ml4 12891 2010-03-30 11:40:02Z herbelin $ i*)
(*i camlp4use: "pr_o.cmo" i*)
@@ -91,6 +91,14 @@ let error_utf8 cs =
Stream.junk cs; (* consume the char to avoid read it and fail again *)
err (bp, bp+1) Illegal_character
+let utf8_char_size cs = function
+ (* Utf8 leading byte *)
+ | '\x00'..'\x7F' -> 1
+ | '\xC0'..'\xDF' -> 2
+ | '\xE0'..'\xEF' -> 3
+ | '\xF0'..'\xF7' -> 4
+ | _ (* '\x80'..\xBF'|'\xF8'..'\xFF' *) -> error_utf8 cs
+
let njunk n = Util.repeat n Stream.junk
let check_utf8_trailing_byte cs c =
@@ -355,14 +363,8 @@ and progress_utf8 last nj n c tt cs =
with Not_found ->
last
-and progress_from_byte last nj tt cs = function
- (* Utf8 leading byte *)
- | '\x00'..'\x7F' as c -> progress_utf8 last nj 1 c tt cs
- | '\xC0'..'\xDF' as c -> progress_utf8 last nj 2 c tt cs
- | '\xE0'..'\xEF' as c -> progress_utf8 last nj 3 c tt cs
- | '\xF0'..'\xF7' as c -> progress_utf8 last nj 4 c tt cs
- | _ (* '\x80'..\xBF'|'\xF8'..'\xFF' *) ->
- error_utf8 cs
+and progress_from_byte last nj tt cs c =
+ progress_utf8 last nj (utf8_char_size cs c) c tt cs
(* Must be a special token *)
let process_chars bp c cs =
@@ -370,7 +372,10 @@ let process_chars bp c cs =
let ep = Stream.count cs in
match t with
| Some t -> (("", t), (bp, ep))
- | None -> err (bp, ep) Undefined_token
+ | None ->
+ let ep' = bp + utf8_char_size cs c in
+ njunk (ep' - ep) cs;
+ err (bp, ep') Undefined_token
let parse_after_dollar bp =
parser
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 3b433498..f52ebc76 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: pptactic.ml 11784 2009-01-14 11:36:32Z herbelin $ *)
+(* $Id: pptactic.ml 12581 2009-12-13 15:02:33Z herbelin $ *)
open Pp
open Names
@@ -378,7 +378,7 @@ let pr_as_ipat = function
let pr_as_name = function
| Anonymous -> mt ()
- | Name id -> str "as " ++ pr_lident (dummy_loc,id)
+ | Name id -> str " as " ++ pr_lident (dummy_loc,id)
let pr_pose_as_style prc na c =
spc() ++ prc c ++ pr_as_name na
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index c2d8921e..abe4fcc1 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: cases.ml 12167 2009-06-06 20:07:22Z herbelin $ *)
+(* $Id: cases.ml 13112 2010-06-10 19:58:23Z herbelin $ *)
open Util
open Names
@@ -851,7 +851,7 @@ let rec map_predicate f k ccl = function
| Abstract _ :: rest ->
map_predicate f (k+1) ccl rest
-let noccurn_predicate = map_predicate noccurn
+let noccur_predicate_between n = map_predicate (noccur_between n)
let liftn_predicate n = map_predicate (liftn n)
@@ -1122,13 +1122,16 @@ let build_branch current deps (realnames,dep) pb eqns const_info =
(* into "Gamma; typs; curalias |- tms" *)
let tomatch = lift_tomatch_stack const_info.cs_nargs pb.tomatch in
+ let pred_is_not_dep =
+ noccur_predicate_between 1 (List.length realnames + 1) pb.pred tomatch in
+
let typs'' =
list_map2_i
(fun i (na,t) deps ->
let dep = match dep with
| Name _ as na',k -> (if na <> Anonymous then na else na'),k
| Anonymous,KnownNotDep ->
- if deps = [] && noccurn_predicate 1 pb.pred tomatch then
+ if deps = [] && pred_is_not_dep then
(Anonymous,KnownNotDep)
else
(force_name na,KnownDep)
@@ -1801,7 +1804,8 @@ let prepare_predicate loc typing_fun evdref env tomatchs sign tycon pred =
let t2 = mkExistential env ~src:(loc, CasesType) evdref2 in
let arsign = extract_arity_signature env tomatchs sign in
let names2 = List.rev (List.map (List.map pi1) arsign) in
- let nal2,pred2 = build_initial_predicate KnownNotDep names2 t2 in
+ let pred2 = lift (List.length names2) t2 in
+ let nal2,pred2 = build_initial_predicate KnownNotDep names2 pred2 in
[evdref, nal1, pred1; evdref2, nal2, pred2])
(* Some type annotation *)
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 51952f4f..0bfef04a 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: clenv.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: clenv.ml 13126 2010-06-13 11:09:51Z herbelin $ *)
open Pp
open Util
@@ -410,8 +410,9 @@ let clenv_unify_binding_type clenv c t u =
try
let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd c t u in
TypeProcessed, { clenv with evd = evd }, c
- with e when precatchable_exception e ->
- TypeNotProcessed, clenv, c
+ with
+ | PretypeError (_,NotClean _) as e -> raise e
+ | e when precatchable_exception e -> TypeNotProcessed, clenv, c
let clenv_assign_binding clenv k (sigma,c) =
let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
@@ -436,11 +437,11 @@ let clenv_match_args bl clenv =
clenv_assign_binding clenv k sc)
clenv bl
+exception NoSuchBinding
+
let clenv_constrain_last_binding c clenv =
let all_mvs = collect_metas clenv.templval.rebus in
- let k =
- try list_last all_mvs
- with Failure _ -> anomaly "clenv_constrain_with_bindings" in
+ let k = try list_last all_mvs with Failure _ -> raise NoSuchBinding in
clenv_assign_binding clenv k (Evd.empty,c)
let clenv_constrain_dep_args hyps_only bl clenv =
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
index 9b2d6e29..4c5535b3 100644
--- a/pretyping/clenv.mli
+++ b/pretyping/clenv.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: clenv.mli 10856 2008-04-27 16:15:34Z herbelin $ i*)
+(*i $Id: clenv.mli 13126 2010-06-13 11:09:51Z herbelin $ i*)
(*i*)
open Util
@@ -94,6 +94,8 @@ type arg_bindings = open_constr explicit_bindings
val clenv_independent : clausenv -> metavariable list
val clenv_missing : clausenv -> metavariable list
+(** for the purpose of inversion tactics *)
+exception NoSuchBinding
val clenv_constrain_last_binding : constr -> clausenv -> clausenv
(* defines metas corresponding to the name of the bindings *)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 73dc5d46..20cbba94 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: detyping.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: detyping.ml 12887 2010-03-27 15:57:02Z herbelin $ *)
open Pp
open Util
@@ -329,7 +329,6 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
n, aliastyp, Some typ
in
let constructs = Array.init (Array.length bl) (fun i -> (indsp,i+1)) in
- let eqnl = detype_eqns constructs consnargsl bl in
let tag =
try
if !Flags.raw_print then
@@ -357,8 +356,10 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
RIf (dl,tomatch,(alias,pred),
Option.get nondepbrs.(0),Option.get nondepbrs.(1))
else
+ let eqnl = detype_eqns constructs consnargsl bl in
RCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl)
| _ ->
+ let eqnl = detype_eqns constructs consnargsl bl in
RCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl)
let detype_sort = function
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 043a326d..18e79e85 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: evarconv.ml 12205 2009-06-22 16:10:15Z barras $ *)
+(* $Id: evarconv.ml 12268 2009-08-11 09:02:16Z herbelin $ *)
open Pp
open Util
@@ -66,6 +66,10 @@ let apprec_nohdbeta env evd c =
| (Case _ | Fix _) -> applist (evar_apprec env evd [] c)
| _ -> c
+let position_problem l2r = function
+ | CONV -> None
+ | CUMUL -> Some l2r
+
(* [check_conv_record (t1,l1) (t2,l2)] tries to decompose the problem
(t1 l1) = (t2 l2) into a problem
@@ -177,9 +181,11 @@ let rec evar_conv_x env evd pbty term1 term2 =
let term1 = apprec_nohdbeta env evd term1 in
let term2 = apprec_nohdbeta env evd term2 in
if is_undefined_evar evd term1 then
- solve_simple_eqn evar_conv_x env evd (pbty,destEvar term1,term2)
+ solve_simple_eqn evar_conv_x env evd
+ (position_problem true pbty,destEvar term1,term2)
else if is_undefined_evar evd term2 then
- solve_simple_eqn evar_conv_x env evd (pbty,destEvar term2,term1)
+ solve_simple_eqn evar_conv_x env evd
+ (position_problem false pbty,destEvar term2,term1)
else
evar_eqappr_x env evd pbty
(decompose_app term1) (decompose_app term2)
@@ -193,14 +199,14 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
ise_and i
[(fun i -> solve_simple_eqn evar_conv_x env i
- (pbty,ev2,applist(term1,deb1)));
+ (position_problem false pbty,ev2,applist(term1,deb1)));
(fun i -> ise_list2 i
(fun i -> evar_conv_x env i CONV) rest1 l2)]
else
let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in
ise_and i
[(fun i -> solve_simple_eqn evar_conv_x env i
- (pbty,ev1,applist(term2,deb2)));
+ (position_problem true pbty,ev1,applist(term2,deb2)));
(fun i -> ise_list2 i
(fun i -> evar_conv_x env i CONV) l1 rest2)]
and f2 i =
@@ -224,7 +230,8 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
(* Preserve generality (except that CCI has no eta-conversion) *)
let t2 = nf_evar (evars_of evd) (applist appr2) in
let t2 = solve_pattern_eqn env l1 t2 in
- solve_simple_eqn evar_conv_x env evd (pbty,ev1,t2)
+ solve_simple_eqn evar_conv_x env evd
+ (position_problem true pbty,ev1,t2)
else if
List.length l1 <= List.length l2
then
@@ -256,7 +263,8 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
(* Preserve generality (except that CCI has no eta-conversion) *)
let t1 = nf_evar (evars_of evd) (applist appr1) in
let t1 = solve_pattern_eqn env l2 t1 in
- solve_simple_eqn evar_conv_x env evd (pbty,ev2,t1)
+ solve_simple_eqn evar_conv_x env evd
+ (position_problem false pbty,ev2,t1)
else if
List.length l2 <= List.length l1
then
@@ -324,7 +332,8 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
(* Preserve generality (except that CCI has no eta-conversion) *)
let t2 = nf_evar (evars_of evd) (applist appr2) in
let t2 = solve_pattern_eqn env l1 t2 in
- solve_simple_eqn evar_conv_x env evd (pbty,ev1,t2)
+ solve_simple_eqn evar_conv_x env evd
+ (position_problem true pbty,ev1,t2)
else
(* Postpone the use of an heuristic *)
add_conv_pb (pbty,env,applist appr1,applist appr2) evd,
@@ -339,7 +348,8 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
(* Preserve generality (except that CCI has no eta-conversion) *)
let t1 = nf_evar (evars_of evd) (applist appr1) in
let t1 = solve_pattern_eqn env l2 t1 in
- solve_simple_eqn evar_conv_x env evd (pbty,ev2,t1)
+ solve_simple_eqn evar_conv_x env evd
+ (position_problem false pbty,ev2,t1)
else
(* Postpone the use of an heuristic *)
add_conv_pb (pbty,env,applist appr1,applist appr2) evd,
@@ -505,7 +515,7 @@ let first_order_unification env evd (ev1,l1) (term2,l2) =
if is_defined_evar i ev1 then
evar_conv_x env i CONV t2 (mkEvar ev1)
else
- solve_simple_eqn ~choose:true evar_conv_x env i (CONV,ev1,t2))]
+ solve_simple_eqn ~choose:true evar_conv_x env i (None,ev1,t2))]
let choose_less_dependent_instance evk evd term args =
let evi = Evd.find (evars_of evd) evk in
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 994da427..fbaac79b 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: evarutil.ml 12107 2009-04-25 19:58:24Z herbelin $ *)
+(* $Id: evarutil.ml 13116 2010-06-12 15:18:07Z herbelin $ *)
open Util
open Pp
@@ -113,11 +113,27 @@ let push_dependent_evars sigma emap =
(sigma',emap') (collect_evars emap' ccl))
emap (sigma,emap)
+let push_duplicated_evars sigma emap c =
+ let rec collrec (one,(sigma,emap) as acc) c =
+ match kind_of_term c with
+ | Evar (evk,_) when not (Evd.mem sigma evk) ->
+ if List.mem evk one then
+ let sigma' = Evd.add sigma evk (Evd.find emap evk) in
+ let emap' = Evd.remove emap evk in
+ (one,(sigma',emap'))
+ else
+ (evk::one,(sigma,emap))
+ | _ ->
+ fold_constr collrec acc c
+ in
+ snd (collrec ([],(sigma,emap)) c)
+
(* replaces a mapping of existentials into a mapping of metas.
Problem if an evar appears in the type of another one (pops anomaly) *)
let evars_to_metas sigma (emap, c) =
let emap = nf_evars emap in
let sigma',emap' = push_dependent_evars sigma emap in
+ let sigma',emap' = push_duplicated_evars sigma' emap' c in
let change_exist evar =
let ty = nf_betaiota emap (existential_type emap evar) in
let n = new_meta() in
@@ -559,6 +575,7 @@ let rec expansions_of_var env x =
*)
exception NotUnique
+exception NotUniqueInType of types
type evar_projection =
| ProjectVar
@@ -570,12 +587,13 @@ let rec find_projectable_vars with_evars env sigma y subst =
if y = y' or expand_var env y = expand_var env y'
then (idc,(y'=y,(id,ProjectVar)))
else if with_evars & isEvar y' then
+ (* TODO: infer conditions for being of unifiable types *)
let (evk,argsv as t) = destEvar y' in
let evi = Evd.find sigma evk in
let subst = make_projectable_subst sigma evi argsv in
let l = find_projectable_vars with_evars env sigma y subst in
match l with
- | [id',p] -> (idc,(true,(id,ProjectEvar (t,evi,id',p))))
+ | [id',p] -> (idc,(true,(id,ProjectEvar(t,evi,id',p))))
| _ -> failwith ""
else failwith "" in
let l = map_succeed is_projectable subst in
@@ -596,6 +614,12 @@ let project_with_effects env sigma effects t subst =
effects := p :: !effects;
c
+let rec find_solution_type evarenv = function
+ | (id,ProjectVar)::l -> pi3 (lookup_named id evarenv)
+ | [id,ProjectEvar _] -> (* bugged *) pi3 (lookup_named id evarenv)
+ | (id,ProjectEvar _)::l -> find_solution_type evarenv l
+ | [] -> assert false
+
(* In case the solution to a projection problem requires the instantiation of
* subsidiary evars, [do_projection_effects] performs them; it
* also try to instantiate the type of those subsidiary evars if their
@@ -709,7 +733,7 @@ let filter_along f projs v =
* such that "hyps' |- ?e : T"
*)
-let do_restrict_hyps_virtual evd evk filter =
+let restrict_hyps evd evk filter =
(* What to do with dependencies?
Assume we have x:A, y:B(x), z:C(x,y) |- ?e:T(x,y,z) and restrict on y.
- If y is in a non-erasable position in C(x,y) (i.e. it is not below an
@@ -726,15 +750,15 @@ let do_restrict_hyps_virtual evd evk filter =
let filter,_ = List.fold_right (fun oldb (l,filter) ->
if oldb then List.hd filter::l,List.tl filter else (false::l,filter))
oldfilter ([],List.rev filter) in
- new_evar evd env ~src:(evar_source evk evd)
- ~filter:filter evi.evar_concl
+ (env,evar_source evk evd,filter,evi.evar_concl)
let do_restrict_hyps evd evk projs =
let filter = List.map filter_of_projection projs in
if List.for_all (fun x -> x) filter then
evd,evk
else
- let evd,nc = do_restrict_hyps_virtual evd evk filter in
+ let env,src,filter,ccl = restrict_hyps evd evk filter in
+ let evd,nc = new_evar evd env ~src ~filter ccl in
let evd = Evd.evar_define evk nc evd in
let evk',_ = destEvar nc in
evd,evk'
@@ -854,7 +878,9 @@ let rec invert_definition choose env evd (evk,argsv as ev) rhs =
let c, p = match sols with
| [] -> raise Not_found
| [id,p] -> (mkVar id, p)
- | (id,p)::_::_ -> if choose then (mkVar id, p) else raise NotUnique
+ | (id,p)::_::_ ->
+ if choose then (mkVar id, p)
+ else raise (NotUniqueInType(find_solution_type (evar_env evi) sols))
in
let ty = lazy (Retyping.get_type_of env (evars_of !evdref) t) in
let evd = do_projection_effects evar_define env ty !evdref p in
@@ -862,14 +888,15 @@ let rec invert_definition choose env evd (evk,argsv as ev) rhs =
c
with
| Not_found -> raise (NotInvertibleUsingOurAlgorithm t)
- | NotUnique ->
+ | NotUniqueInType ty ->
if not !progress then raise NotEnoughInformationToProgress;
(* No unique projection but still restrict to where it is possible *)
let ts = expansions_of_var env t in
let test c = isEvar c or List.mem c ts in
let filter = array_map_to_list test argsv in
let args' = filter_along (fun x -> x) filter argsv in
- let evd,evar = do_restrict_hyps_virtual !evdref evk filter in
+ let evarenv,src,filter,_ = restrict_hyps !evdref evk filter in
+ let evd,evar = new_evar !evdref evarenv ~src ~filter ty in
let evk',_ = destEvar evar in
let pb = (Reduction.CONV,env,mkEvar(evk',args'),t) in
evdref := Evd.add_conv_pb pb evd;
@@ -1122,6 +1149,24 @@ let solve_refl conv_algo env evd evk argsv1 argsv2 =
let pb = (Reduction.CONV,env,mkEvar(evk,argsv1),mkEvar(evk,argsv2)) in
Evd.add_conv_pb pb evd
+(* Util *)
+
+let check_instance_type conv_algo env evd ev1 t2 =
+ let t2 = nf_evar (evars_of evd) t2 in
+ if has_undefined_evars evd t2 then
+ (* May contain larger constraints than needed: don't want to
+ commit to an equal solution while only subtyping is requested *)
+ evd
+ else
+ let typ2 = Retyping.get_type_of env (evars_of evd) (refresh_universes t2) in
+ if isEvar typ2 then (* Don't want to commit too early too *) evd
+ else
+ let typ1 = existential_type (evars_of evd) ev1 in
+ let evd,b = conv_algo env evd Reduction.CUMUL typ2 typ1 in
+ if b then evd else
+ user_err_loc (fst (evar_source (fst ev1) evd),"",
+ str "Unable to find a well-typed instantiation")
+
(* Tries to solve problem t1 = t2.
* Precondition: t1 is an uninstantiated evar
* Returns an optional list of evars that were instantiated, or None
@@ -1136,15 +1181,23 @@ let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1)
if evk1 = evk2 then
solve_refl conv_algo env evd evk1 args1 args2
else
- if pbty = Reduction.CONV
+ if pbty = None
then solve_evar_evar evar_define env evd ev1 ev2
- else add_conv_pb (pbty,env,mkEvar ev1,t2) evd
+ else if pbty = Some true then
+ add_conv_pb (Reduction.CUMUL,env,mkEvar ev1,t2) evd
+ else
+ add_conv_pb (Reduction.CUMUL,env,t2,mkEvar ev1) evd
| _ ->
+ let evd =
+ if pbty = Some false then
+ check_instance_type conv_algo env evd ev1 t2
+ else
+ evd in
let evd = evar_define ~choose env ev1 t2 evd in
let evm = evars_of evd in
let evi = Evd.find evm evk1 in
if occur_existential evm evi.evar_concl then
- let evenv = evar_env evi in
+ let evenv = evar_unfiltered_env evi in
let evc = nf_isevar evd evi.evar_concl in
match evi.evar_body with
| Evar_defined body ->
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index cb54f400..eef41da3 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: evarutil.mli 12053 2009-04-06 16:20:42Z msozeau $ i*)
+(*i $Id: evarutil.mli 12268 2009-08-11 09:02:16Z herbelin $ i*)
(*i*)
open Util
@@ -80,7 +80,7 @@ val solve_refl :
evar_defs
val solve_simple_eqn :
(env -> evar_defs -> conv_pb -> constr -> constr -> evar_defs * bool)
- -> ?choose:bool -> env -> evar_defs -> conv_pb * existential * constr ->
+ -> ?choose:bool -> env -> evar_defs -> bool option * existential * constr ->
evar_defs * bool
(* [check_evars env initial_sigma extended_sigma c] fails if some
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 740b2ca8..f579afa6 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: tacred.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: tacred.ml 12233 2009-07-08 22:50:56Z herbelin $ *)
open Pp
open Util
@@ -137,20 +137,27 @@ let _ =
Summary.survive_module = false;
Summary.survive_section = false }
-(* Check that c is an "elimination constant"
+(* [compute_consteval] determines whether c is an "elimination constant"
- either [xn:An]..[x1:A1](<P>Case (Rel i) of f1..fk end g1 ..gp)
+ either [yn:Tn]..[y1:T1](match yi with f1..fk end g1 ..gp)
- or [xn:An]..[x1:A1](Fix(f|t) (Rel i1) ..(Rel ip))
- with i1..ip distinct variables not occuring in t
+ or [yn:Tn]..[y1:T1](Fix(f|t) yi1..yip)
+ with yi1..yip distinct variables among the yi, not occurring in t
- In the second case, keep relevenant information ([i1,Ai1;..;ip,Aip],n)
- in order to compute an equivalent of Fix(f|t)[xi<-ai] as
+ In the second case, [check_fix_reversibility [T1;...;Tn] args fix]
+ checks that [args] is a subset of disjoint variables in y1..yn (a necessary
+ condition for reversibility). It also returns the relevant
+ information ([i1,Ti1;..;ip,Tip],n) in order to compute an
+ equivalent of Fix(f|t) such that
- [yip:Bip]..[yi1:Bi1](F bn..b1)
- == [yip:Bip]..[yi1:Bi1](Fix(f|t)[xi<-ai] (Rel p)..(Rel 1))
+ g := [xp:Tip']..[x1:Ti1'](f a1..an)
+ == [xp:Tip']..[x1:Ti1'](Fix(f|t) yi1..yip)
- with bj=aj if j<>ik and bj=(Rel c) and Bic=Aic[xn..xic-1 <- an..aic-1]
+ with a_k:=y_k if k<>i_j, a_k:=args_k otherwise, and
+ Tij':=Tij[x1..xi(j-1) <- a1..ai(j-1)]
+
+ Note that the types Tk, when no i_j=k, must not be dependent on
+ the xp..x1.
*)
let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) =
@@ -172,8 +179,14 @@ let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) =
| _ ->
raise Elimconst) args
in
- if not (list_distinct (List.map fst li)) then
+ let reversible_rels = List.map fst li in
+ if not (list_distinct reversible_rels) then
raise Elimconst;
+ list_iter_i (fun i t_i ->
+ if not (List.mem_assoc (i+1) li) then
+ let fvs = List.map ((+) (i+1)) (Intset.elements (free_rels t_i)) in
+ if list_intersect fvs reversible_rels <> [] then raise Elimconst)
+ labs;
let k = lv.(i) in
if k < nargs then
(* Such an optimisation would need eta-expansion
@@ -294,19 +307,22 @@ let rev_firstn_liftn fn ln =
(* If f is bound to EliminationFix (n',infos), then n' is the minimal
number of args for starting the reduction and infos is
(nbfix,[(yi1,Ti1);...;(yip,Tip)],n) indicating that f converts
- to some [y1:T1,...,yn:Tn](Fix(..) yip .. yi1) where we can remark that
- yij = Rel(n+1-j)
+ to some [y1:T1,...,yn:Tn](Fix(..) yip .. yi1) where the y_{i_j} consist in a
+ disjoint subset of the yi, i.e. 1 <= ij <= n and the ij are disjoint (in
+ particular, p <= n).
+
+ f is applied to largs := arg1 .. argn and we need for recursive
+ calls to build the function
- f is applied to largs and we need for recursive calls to build the function
g := [xp:Tip',...,x1:Ti1'](f a1 ... an)
s.t. (g u1 ... up) reduces to (Fix(..) u1 ... up)
This is made possible by setting
- a_k:=z_j if k=i_j
- a_k:=y_k otherwise
+ a_k:=x_j if k=i_j for some j
+ a_k:=arg_k otherwise
- The type Tij' is Tij[yn..yi(j-1)..y1 <- ai(j-1)..a1]
+ The type Tij' is Tij[yi(j-1)..y1 <- ai(j-1)..a1]
*)
let x = Name (id_of_string "x")
@@ -328,7 +344,7 @@ let make_elim_fun (names,(nbfix,lv,n)) largs =
| Some (minargs,ref) ->
let body = applistc (mkEvalRef ref) la in
let g =
- list_fold_left_i (fun q (* j from comment is n+1-q *) c (ij,tij) ->
+ list_fold_left_i (fun q (* j = n+1-q *) c (ij,tij) ->
let subst = List.map (lift (-q)) (list_firstn (n-ij) la) in
let tij' = substl (List.rev subst) tij in
mkLambda (x,tij',c)) 1 body (List.rev lv)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index bfd601e2..c92f1fc6 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: unification.ml 12163 2009-06-06 17:36:47Z herbelin $ *)
+(* $Id: unification.ml 12268 2009-08-11 09:02:16Z herbelin $ *)
open Pp
open Util
@@ -517,7 +517,7 @@ let order_metas metas =
(* Solve an equation ?n[x1=u1..xn=un] = t where ?n is an evar *)
let solve_simple_evar_eqn env evd ev rhs =
- let evd,b = solve_simple_eqn Evarconv.evar_conv_x env evd (CONV,ev,rhs) in
+ let evd,b = solve_simple_eqn Evarconv.evar_conv_x env evd (None,ev,rhs) in
if not b then error_cannot_unify env (evars_of evd) (mkEvar ev,rhs);
let (evd,b) = Evarconv.consider_remaining_unif_problems env evd in
if not b then error "Cannot solve unification constraints";
diff --git a/proofs/decl_mode.ml b/proofs/decl_mode.ml
index f8fc4e87..134a4d8b 100644
--- a/proofs/decl_mode.ml
+++ b/proofs/decl_mode.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: decl_mode.ml 10739 2008-04-01 14:45:20Z herbelin $ i*)
+(*i $Id: decl_mode.ml 12422 2009-10-27 08:42:49Z corbinea $ i*)
open Names
open Term
@@ -45,7 +45,7 @@ type split_tree=
| Split_patt of Idset.t * inductive *
(bool array * (Idset.t * split_tree) option) array
| Close_patt of split_tree
- | End_patt of (identifier * int)
+ | End_patt of (identifier * (int * int))
type elim_kind =
EK_dep of split_tree
@@ -124,3 +124,4 @@ let get_last env =
try
let (id,_,_) = List.hd (Environ.named_context env) in id
with Invalid_argument _ -> error "no previous statement to use"
+
diff --git a/proofs/decl_mode.mli b/proofs/decl_mode.mli
index 77bee313..bcfd6a96 100644
--- a/proofs/decl_mode.mli
+++ b/proofs/decl_mode.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: decl_mode.mli 10739 2008-04-01 14:45:20Z herbelin $ *)
+(* $Id: decl_mode.mli 12422 2009-10-27 08:42:49Z corbinea $ *)
open Names
open Term
@@ -33,7 +33,7 @@ type split_tree=
| Split_patt of Idset.t * inductive *
(bool array * (Idset.t * split_tree) option) array
| Close_patt of split_tree
- | End_patt of (identifier * int)
+ | End_patt of (identifier * (int * int))
type elim_kind =
EK_dep of split_tree
diff --git a/proofs/logic.ml b/proofs/logic.ml
index caf6f56b..c019d45f 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: logic.ml 12168 2009-06-06 21:34:37Z herbelin $ *)
+(* $Id: logic.ml 12240 2009-07-15 09:52:52Z herbelin $ *)
open Pp
open Util
@@ -438,7 +438,7 @@ and mk_casegoals sigma goal goalacc p c =
let (acc'',pt) = mk_hdgoals sigma goal acc' p in
let pj = {uj_val=p; uj_type=pt} in
let indspec =
- try find_mrectype env sigma ct
+ try find_mrectype env sigma (nf_evar sigma ct)
with Not_found -> anomaly "mk_casegoals" in
let (lbrty,conclty) =
type_case_branches_with_names env indspec pj c in
diff --git a/scripts/coqc.ml b/scripts/coqc.ml
index 784e2d51..69357b2f 100644
--- a/scripts/coqc.ml
+++ b/scripts/coqc.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coqc.ml 11749 2009-01-05 14:01:04Z notin $ *)
+(* $Id: coqc.ml 12911 2010-04-09 10:08:37Z herbelin $ *)
(* Afin de rendre Coq plus portable, ce programme Caml remplace le script
coqc.
@@ -126,8 +126,8 @@ let parse_args () =
parse (cfiles,args) rem
| ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()
- | ("-I"|"-include"|"-outputstate"
- |"-inputstate"|"-is"|"-load-vernac-source"|"-l"|"-load-vernac-object"
+ | ("-outputstate"|"-inputstate"|"-is"
+ |"-load-vernac-source"|"-l"|"-load-vernac-object"
|"-load-ml-source"|"-require"|"-load-ml-object"|"-user"
|"-init-file" | "-dump-glob" | "-coqlib" as o) :: rem ->
begin
@@ -135,7 +135,17 @@ let parse_args () =
| s :: rem' -> parse (cfiles,s::o::args) rem'
| [] -> usage ()
end
- | "-R" as o :: s :: t :: rem -> parse (cfiles,t::s::o::args) rem
+ | ("-I"|"-include" as o) :: rem ->
+ begin
+ match rem with
+ | s :: "-as" :: t :: rem' -> parse (cfiles,t::"-as"::s::o::args) rem'
+ | s :: "-as" :: [] -> usage ()
+ | s :: rem' -> parse (cfiles,s::o::args) rem'
+ | [] -> usage ()
+ end
+ | "-R" :: s :: "-as" :: t :: rem -> parse (cfiles,t::"-as"::s::"-R"::args) rem
+ | "-R" :: s :: "-as" :: [] -> usage ()
+ | "-R" :: s :: t :: rem -> parse (cfiles,t::s::"-R"::args) rem
| ("-notactics"|"-debug"|"-nolib"
|"-debugVM"|"-alltransp"|"-VMno"
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index 9a7d30b1..ee8ef1d9 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coqmktop.ml 11784 2009-01-14 11:36:32Z herbelin $ *)
+(* $Id: coqmktop.ml 12874 2010-03-19 23:15:52Z herbelin $ *)
(* coqmktop is a script to link Coq, analogous to ocamlmktop.
The command line contains options specific to coqmktop, options for the
@@ -277,7 +277,7 @@ let main () =
(*file for dynlink *)
let dynlink=
if not (!opt || !top) then
- [(print_int 2; tmp_dynlink())]
+ [tmp_dynlink()]
else
[]
in
diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml
index c99884c0..62824670 100644
--- a/tactics/decl_interp.ml
+++ b/tactics/decl_interp.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: decl_interp.ml 11576 2008-11-10 19:13:15Z msozeau $ i*)
+(*i $Id: decl_interp.ml 12422 2009-10-27 08:42:49Z corbinea $ i*)
open Util
open Names
@@ -334,7 +334,7 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
if List.length params <> expected then
errorlabstrm "suppose it is"
(str "Wrong number of extra arguments: " ++
- (if expected = 0 then str "none" else int expected) ++
+ (if expected = 0 then str "none" else int expected) ++ spc () ++
str "expected.") in
let app_ind =
let rind = RRef (dummy_loc,Libnames.IndRef pinfo.per_ind) in
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml
index 62a8ddfc..67d1d41a 100644
--- a/tactics/decl_proof_instr.ml
+++ b/tactics/decl_proof_instr.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: decl_proof_instr.ml 12135 2009-05-20 14:49:23Z herbelin $ *)
+(* $Id: decl_proof_instr.ml 12422 2009-10-27 08:42:49Z corbinea $ *)
open Util
open Pp
@@ -1161,7 +1161,7 @@ let case_tac params pat_info hyps gls0 =
let clause = build_dep_clause params pat_info per_info hyps gls0 in
let ninfo1 = {pm_stack=Suppose_case::info.pm_stack} in
let nek =
- register_dep_subcase (id,List.length hyps) (pf_env gls0) per_info
+ register_dep_subcase (id,(List.length params,List.length hyps)) (pf_env gls0) per_info
pat_info.pat_pat ek in
let ninfo2 = {pm_stack=Per(et,per_info,nek,id::old_clauses)::rest} in
tclTHENS (assert_postpone id clause)
@@ -1227,6 +1227,7 @@ let hrec_for fix_id per_info gls obj_id =
let hd2 = applist (mkVar fix_id,args@[obj]) in
compose_lam rc (whd_beta gls.sigma hd2)
+
let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
match tree, objs with
Close_patt t,_ ->
@@ -1235,16 +1236,19 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
| Skip_patt (_,t),skipped::next_objs ->
let args0 = push_arg skipped args in
execute_cases fix_name per_info tacnext args0 next_objs nhrec t gls
- | End_patt (id,nhyps),[] ->
+ | End_patt (id,(nparams,nhyps)),[] ->
begin
match List.assoc id args with
[None,br_args] ->
- let metas =
- list_tabulate (fun n -> mkMeta (succ n)) nhyps in
+ let all_metas =
+ list_tabulate (fun n -> mkMeta (succ n)) (nparams + nhyps) in
+ let param_metas,hyp_metas = list_chop nparams all_metas in
tclTHEN
(tclDO nhrec introf)
(tacnext
- (applist (mkVar id,List.rev_append br_args metas))) gls
+ (applist (mkVar id,
+ List.append param_metas
+ (List.rev_append br_args hyp_metas)))) gls
| _ -> anomaly "wrong stack size"
end
| Split_patt (ids,ind,br), casee::next_objs ->
@@ -1318,7 +1322,19 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
| End_patt (_,_) , _ :: _ ->
anomaly "execute_cases : End of branch with garbage left"
-
+let understand_my_constr c gls =
+ let env = pf_env gls in
+ let nc = names_of_rel_context env in
+ let rawc = Detyping.detype false [] nc c in
+ let rec frob = function REvar _ -> RHole (dummy_loc,QuestionMark Expand) | rc -> map_rawconstr frob rc in
+ Pretyping.Default.understand_tcc (sig_sig gls) env ~expected_type:(pf_concl gls) (frob rawc)
+
+let set_refine,my_refine =
+let refine = ref (fun (_:open_constr) -> (assert false : tactic) ) in
+((fun tac -> refine:= tac),
+(fun c gls ->
+ let oc = understand_my_constr c gls in
+ !refine oc gls))
(* end focus/claim *)
@@ -1361,7 +1377,7 @@ let end_tac et2 gls =
| ET_Case_analysis,EK_dep tree ->
execute_cases Anonymous pi
(fun c -> tclTHENLIST
- [refine c;
+ [my_refine c;
clear clauses;
justification assumption])
(initial_instance_stack clauses) [pi.per_casee] 0 tree
@@ -1382,7 +1398,7 @@ let end_tac et2 gls =
(fun c ->
tclTHENLIST
[clear [fix_id];
- refine c;
+ my_refine c;
clear clauses;
justification assumption])
(initial_instance_stack clauses)
diff --git a/tactics/decl_proof_instr.mli b/tactics/decl_proof_instr.mli
index 877c8047..5f4a0485 100644
--- a/tactics/decl_proof_instr.mli
+++ b/tactics/decl_proof_instr.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: decl_proof_instr.mli 11481 2008-10-20 19:23:51Z herbelin $ *)
+(* $Id: decl_proof_instr.mli 12422 2009-10-27 08:42:49Z corbinea $ *)
open Refiner
open Names
@@ -42,20 +42,20 @@ val execute_cases :
Term.constr list -> int -> Decl_mode.split_tree -> Proof_type.tactic
val tree_of_pats :
- identifier * int -> (Rawterm.cases_pattern*recpath) list list ->
+ identifier * (int * int) -> (Rawterm.cases_pattern*recpath) list list ->
split_tree
val add_branch :
- identifier * int -> (Rawterm.cases_pattern*recpath) list list ->
+ identifier * (int * int) -> (Rawterm.cases_pattern*recpath) list list ->
split_tree -> split_tree
val append_branch :
- identifier * int -> int -> (Rawterm.cases_pattern*recpath) list list ->
+ identifier *(int * int) -> int -> (Rawterm.cases_pattern*recpath) list list ->
(Names.Idset.t * Decl_mode.split_tree) option ->
(Names.Idset.t * Decl_mode.split_tree) option
val append_tree :
- identifier * int -> int -> (Rawterm.cases_pattern*recpath) list list ->
+ identifier * (int * int) -> int -> (Rawterm.cases_pattern*recpath) list list ->
split_tree -> split_tree
val build_dep_clause : Term.types Decl_expr.statement list ->
@@ -65,7 +65,7 @@ val build_dep_clause : Term.types Decl_expr.statement list ->
Decl_expr.hyp list -> Proof_type.goal Tacmach.sigma -> Term.types
val register_dep_subcase :
- Names.identifier * int ->
+ Names.identifier * (int * int) ->
Environ.env ->
Decl_mode.per_info ->
Rawterm.cases_pattern -> Decl_mode.elim_kind -> Decl_mode.elim_kind
@@ -115,3 +115,4 @@ val init_tree:
(Names.Idset.t * Decl_mode.split_tree) option) ->
Decl_mode.split_tree
+val set_refine : (Evd.open_constr -> Proof_type.tactic) -> unit
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 58a00419..bf199379 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: equality.ml 12053 2009-04-06 16:20:42Z msozeau $ *)
+(* $Id: equality.ml 12886 2010-03-27 14:22:00Z herbelin $ *)
open Pp
open Util
@@ -688,6 +688,16 @@ let minimal_free_rels env sigma (c,cty) =
else
(cty',rels')
+(* Like the above, but recurse over all the rels found until there are
+ no more rels to be found *)
+let minimal_free_rels_rec env sigma =
+ let rec minimalrec_free_rels_rec prev_rels (c,cty) =
+ let (cty,direct_rels) = minimal_free_rels env sigma (c,cty) in
+ let combined_rels = Intset.union prev_rels direct_rels in
+ let folder rels i = snd (minimalrec_free_rels_rec rels (c, type_of env sigma (mkRel i)))
+ in (cty, List.fold_left folder combined_rels (Intset.elements (Intset.diff direct_rels prev_rels)))
+ in minimalrec_free_rels_rec Intset.empty
+
(* [sig_clausal_form siglen ty]
Will explode [siglen] [sigS,sigT ]'s on [ty] (depending on the
@@ -706,7 +716,7 @@ let minimal_free_rels env sigma (c,cty) =
WARNING: No checking is done to make sure that the
sigS(or sigT)'s are actually there.
- - Only homogenious pairs are built i.e. pairs where all the
+ - Only homogeneous pairs are built i.e. pairs where all the
dependencies are of the same sort
[sig_clausal_form] proceed as follows: the default tuple is
@@ -747,7 +757,12 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
Evd.existential_opt_value (Evd.evars_of !evdref)
(destEvar ev)
with
- | Some w -> applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
+ | Some w ->
+ let w_type = type_of env sigma w in
+ if Evarconv.e_conv env evdref w_type a then
+ applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
+ else
+ error "Cannot solve a unification problem."
| None -> anomaly "Not enough components to build the dependent tuple"
in
let scf = sigrec_clausal_form siglen ty in
@@ -812,7 +827,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
*)
let make_iterated_tuple env sigma dflt (z,zty) =
- let (zty,rels) = minimal_free_rels env sigma (z,zty) in
+ let (zty,rels) = minimal_free_rels_rec env sigma (z,zty) in
let sort_of_zty = get_sort_of env sigma zty in
let sorted_rels = Sort.list (<) (Intset.elements rels) in
let (tuple,tuplety) =
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 8e517453..4ab40acb 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: hiddentac.ml 12102 2009-04-24 10:48:11Z herbelin $ *)
+(* $Id: hiddentac.ml 13124 2010-06-13 11:09:38Z herbelin $ *)
open Term
open Proof_type
@@ -83,10 +83,10 @@ let h_simple_induction_destruct isrec h =
let h_simple_induction = h_simple_induction_destruct true
let h_simple_destruct = h_simple_induction_destruct false
-let h_induction_destruct isrec ev l =
+let h_induction_destruct ev isrec l =
abstract_tactic (TacInductionDestruct (isrec,ev,List.map (fun (c,e,idl,cl) ->
List.map inj_ia c,Option.map inj_open_wb e,idl,cl) l))
- (induction_destruct ev isrec l)
+ (induction_destruct isrec ev l)
let h_new_induction ev c e idl cl = h_induction_destruct ev true [c,e,idl,cl]
let h_new_destruct ev c e idl cl = h_induction_destruct ev false [c,e,idl,cl]
@@ -105,7 +105,7 @@ let h_revert l = abstract_tactic (TacRevert l) (revert l)
(* Constructors *)
let h_left ev l = abstract_tactic (TacLeft (ev,l)) (left_with_ebindings ev l)
-let h_right ev l = abstract_tactic (TacLeft (ev,l)) (right_with_ebindings ev l)
+let h_right ev l = abstract_tactic (TacRight (ev,l)) (right_with_ebindings ev l)
let h_split ev l = abstract_tactic (TacSplit (ev,false,l)) (split_with_ebindings ev l)
(* Moved to tacinterp because of dependencies in Tacinterp.interp
let h_any_constructor t =
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 977b602e..af204e77 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: inv.ml 11784 2009-01-14 11:36:32Z herbelin $ *)
+(* $Id: inv.ml 12410 2009-10-24 17:23:39Z herbelin $ *)
open Pp
open Util
@@ -291,7 +291,7 @@ let generalizeRewriteIntros tac depids id gls =
let rec tclMAP_i n tacfun = function
| [] -> tclDO n (tacfun None)
| a::l ->
- if n=0 then error "Too much names."
+ if n=0 then error "Too many names."
else tclTHEN (tacfun (Some a)) (tclMAP_i (n-1) tacfun l)
let remember_first_eq id x = if !x = no_move then x := MoveAfter id
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index e798f59a..4cbfa6c2 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: leminv.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: leminv.ml 13126 2010-06-13 11:09:51Z herbelin $ *)
open Pp
open Util
@@ -291,11 +291,15 @@ let add_inversion_lemma_exn na com comsort bool tac =
(* ================================= *)
let lemInv id c gls =
+ ignore (pf_get_hyp gls id); (* ensure id exists *)
try
let clause = mk_clenv_type_of gls c in
let clause = clenv_constrain_last_binding (mkVar id) clause in
Clenvtac.res_pf clause ~allow_K:true gls
with
+ | NoSuchBinding ->
+ errorlabstrm ""
+ (hov 0 (pr_constr c ++ spc () ++ str "does not refer to an inversion lemma."))
| UserError (a,b) ->
errorlabstrm "LemInv"
(str "Cannot refine current goal with the lemma " ++
diff --git a/tactics/refine.ml b/tactics/refine.ml
index 322d25e5..ff3f0887 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: refine.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
+(* $Id: refine.ml 13129 2010-06-13 14:23:55Z herbelin $ *)
(* JCF -- 6 janvier 1998 EXPERIMENTAL *)
@@ -108,6 +108,8 @@ let replace_by_meta env sigma = function
| _ -> invalid_arg "Tcc.replace_by_meta (TO DO)"
*)
in
+ if occur_meta ty then
+ error "Unable to manage a dependent metavariable of higher-order type.";
mkCast (m,DEFAULTcast, ty),[n,ty],[Some th]
exception NoMeta
@@ -189,6 +191,8 @@ let rec compute_metamap env sigma c = match kind_of_term c with
end
| Case (ci,p,cc,v) ->
+ if occur_meta p then
+ error "Unable to manage a metavariable in the return clause of a match.";
(* bof... *)
let nbr = Array.length v in
let v = Array.append [|p;cc|] v in
@@ -380,3 +384,5 @@ let refine (evd,c) gl =
complicated to update meta types when passing through a binder *)
let th = compute_metamap (pf_env gl) evd c in
tclTHEN (Refiner.tclEVARS evd) (tcc_aux [] th) gl
+
+let _ = Decl_proof_instr.set_refine refine (* dirty trick to solve circular dependency *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 71b50b66..5c891c58 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: tacinterp.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
+(* $Id: tacinterp.ml 13130 2010-06-13 18:45:09Z herbelin $ *)
open Constrintern
open Closure
@@ -1096,7 +1096,9 @@ let apply_one_mhyp_context ist env gl lmatch (hypname,patv,pat) lhyps =
match_next_pattern find_next')
with
| PatternMatchingFailure -> apply_one_mhyp_context_rec tl in
- match_next_pattern (fun () -> match_pat lmatch hyp pat) ()
+ match_next_pattern (fun () ->
+ let hyp = if b<>None then refresh_universes_strict hyp else hyp in
+ match_pat lmatch hyp pat) ()
| Some patv ->
match b with
| Some body ->
@@ -1112,7 +1114,9 @@ let apply_one_mhyp_context ist env gl lmatch (hypname,patv,pat) lhyps =
| PatternMatchingFailure ->
match_next_pattern_in_body next_in_body' () in
match_next_pattern_in_typ
- (fun () -> match_pat lmeta hyp pat) ()
+ (fun () ->
+ let hyp = refresh_universes_strict hyp in
+ match_pat lmeta hyp pat) ()
with PatternMatchingFailure -> apply_one_mhyp_context_rec tl
in
match_next_pattern_in_body
@@ -2872,7 +2876,8 @@ let add_tacdef isrec tacl =
(***************************************************************************)
(* Other entry points *)
-let glob_tactic x = intern_tactic (make_empty_glob_sign ()) x
+let glob_tactic x =
+ Flags.with_option strict_check (intern_tactic (make_empty_glob_sign ())) x
let glob_tactic_env l env x =
Flags.with_option strict_check
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0a8b5d01..0a4c0fbe 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: tactics.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
+(* $Id: tactics.ml 12956 2010-04-20 08:49:15Z herbelin $ *)
open Pp
open Util
@@ -249,14 +249,51 @@ let change_option occl t = function
Some id -> change_in_hyp occl t id
| None -> change_in_concl occl t
-let change occl c cls =
+let out_arg = function
+ | ArgVar _ -> anomaly "Unevaluated or_var variable"
+ | ArgArg x -> x
+
+let adjust_clause occl cls =
+ (* warn as much as possible on loss of occurrence information *)
(match cls, occl with
({onhyps=(Some(_::_::_)|None)}
|{onhyps=Some(_::_);concl_occs=((false,_)|(true,_::_))}),
Some _ ->
error "No occurrences expected when changing several hypotheses."
| _ -> ());
- onClauses (change_option occl c) cls
+ (* get at clause from cls if only goal or one hyp specified *)
+ let occl,cls = match occl with
+ | None -> None,cls
+ | Some (occs,c) ->
+ if cls.onhyps=Some[] && occs=all_occurrences then
+ Some (on_snd (List.map out_arg) cls.concl_occs,c),
+ {cls with concl_occs=all_occurrences_expr}
+ else
+ match cls.onhyps with
+ | Some[(occs',id),l] when
+ cls.concl_occs=no_occurrences_expr && occs=all_occurrences ->
+ Some (on_snd (List.map out_arg) occs',c),
+ {cls with onhyps=Some[(all_occurrences_expr,id),l]}
+ | _ ->
+ occl,cls in
+ (* check if cls has still specified occs *)
+ if cls.onhyps <> None &&
+ List.exists (fun ((occs,_),_) -> occs <> all_occurrences_expr)
+ (Option.get cls.onhyps)
+ || cls.concl_occs <> all_occurrences_expr &&
+ cls.concl_occs <> no_occurrences_expr
+ then
+ Flags.if_verbose Pp.msg_warning
+ (if cls.onhyps=Some[] then
+ str "Trailing \"at\" modifier not taken into account."
+ else
+ str "\"at\" modifier in clause \"in\" not taken into account.");
+ (* Anticipate on onClauses which removes concl if not at all occs *)
+ if cls.concl_occs=no_occurrences_expr then cls
+ else {cls with concl_occs=all_occurrences_expr}
+
+let change occl c cls =
+ onClauses (change_option occl c) (adjust_clause occl cls)
(* Pour usage interne (le niveau User est pris en compte par reduce) *)
let red_in_concl = reduct_in_concl (red_product,DEFAULTcast)
@@ -1397,10 +1434,6 @@ let quantify lconstr =
the left of each x1, ...).
*)
-let out_arg = function
- | ArgVar _ -> anomaly "Unevaluated or_var variable"
- | ArgArg x -> x
-
let occurrences_of_hyp id cls =
let rec hyp_occ = function
[] -> None
@@ -2546,6 +2579,7 @@ let induction_tac_felim with_evars indvars scheme gl =
let apply_induction_in_context isrec hyp0 indsign indvars names induct_tac gl =
let env = pf_env gl in
let statlists,lhyp0,indhyps,deps = cook_sign hyp0 indvars env in
+ let deps = List.map (fun (id,c,t)-> (id,c,refresh_universes_strict t)) deps in
let tmpcl = it_mkNamedProd_or_LetIn (pf_concl gl) deps in
let names = compute_induction_names (Array.length indsign) names in
let dephyps = List.map (fun (id,_,_) -> id) deps in
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 1729695d..d3e7da6a 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -8,7 +8,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(*i $Id: tauto.ml4 11739 2009-01-02 19:33:19Z herbelin $ i*)
+(*i $Id: tauto.ml4 12955 2010-04-20 08:10:14Z herbelin $ i*)
open Term
open Hipattern
@@ -20,6 +20,7 @@ open Tacticals
open Tacinterp
open Tactics
open Util
+open Genarg
let assoc_var s ist =
match List.assoc (Names.id_of_string s) ist.lfun with
@@ -97,18 +98,21 @@ let is_conj ist =
let flatten_contravariant_conj ist =
let typ = assoc_var "X1" ist in
let c = assoc_var "X2" ist in
+ let hyp = assoc_var "id" ist in
match match_with_conjunction ~strict:strict_in_contravariant_hyp typ with
| Some (_,args) ->
let i = List.length args in
if not binary_mode || i = 2 then
let newtyp = valueIn (VConstr (List.fold_right mkArrow args c)) in
+ let hyp = valueIn (VConstr hyp) in
let intros =
iter_tac (List.map (fun _ -> <:tactic< intro >>) args)
<:tactic< idtac >> in
<:tactic<
let newtyp := $newtyp in
- assert newtyp by ($intros; apply id; split; assumption);
- clear id
+ let hyp := $hyp in
+ assert newtyp by ($intros; apply hyp; split; assumption);
+ clear hyp
>>
else
<:tactic<fail>>
@@ -129,16 +133,19 @@ let is_disj ist =
let flatten_contravariant_disj ist =
let typ = assoc_var "X1" ist in
let c = assoc_var "X2" ist in
+ let hyp = assoc_var "id" ist in
match match_with_disjunction ~strict:strict_in_contravariant_hyp typ with
| Some (_,args) ->
let i = List.length args in
if not binary_mode || i = 2 then
+ let hyp = valueIn (VConstr hyp) in
iter_tac (list_map_i (fun i arg ->
let typ = valueIn (VConstr (mkArrow arg c)) in
<:tactic<
let typ := $typ in
- assert typ by (intro; apply id; constructor $i; assumption)
- >>) 1 args) <:tactic< clear id >>
+ let hyp := $hyp in
+ assert typ by (intro; apply hyp; constructor $i; assumption)
+ >>) 1 args) <:tactic< let hyp := $hyp in clear hyp >>
else
<:tactic<fail>>
| _ ->
diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v
index 06b4e028..f84d8f58 100644
--- a/theories/FSets/FSetDecide.v
+++ b/theories/FSets/FSetDecide.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id: FSetDecide.v 11699 2008-12-18 11:49:08Z letouzey $ *)
+(* $Id: FSetDecide.v 13199 2010-06-25 22:36:22Z letouzey $ *)
(**************************************************************)
(* FSetDecide.v *)
@@ -346,6 +346,19 @@ the above form:
(** ** Generic Tactics
We begin by defining a few generic, useful tactics. *)
+ (** remove logical hypothesis inter-dependencies (fix #2136). *)
+
+ Ltac no_logical_interdep :=
+ match goal with
+ | H : ?P |- _ =>
+ match type of P with
+ | Prop =>
+ match goal with H' : context [ H ] |- _ => clear dependent H' end
+ | _ => fail
+ end; no_logical_interdep
+ | _ => idtac
+ end.
+
(** [if t then t1 else t2] executes [t] and, if it does not
fail, then [t1] will be applied to all subgoals
produced. If [t] fails, then [t2] is executed. *)
@@ -405,7 +418,7 @@ the above form:
propositions of interest. *)
Inductive FSet_elt_Prop : Prop -> Prop :=
- | eq_Prop : forall (S : Set) (x y : S),
+ | eq_Prop : forall (S : Type) (x y : S),
FSet_elt_Prop (x = y)
| eq_elt_prop : forall x y,
FSet_elt_Prop (E.eq x y)
@@ -660,6 +673,9 @@ the above form:
Ltac fsetdec :=
(** We first unfold any occurrences of [iff]. *)
unfold iff in *;
+ (** We remove dependencies to logical hypothesis. This way,
+ later "clear" will work nicely (see bug #2136) *)
+ no_logical_interdep;
(** We fold occurrences of [not] because it is better for
[intros] to leave us with a goal of [~ P] than a goal of
[False]. *)
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index 3dc6385d..5f18edcd 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Notations.v 11073 2008-06-08 20:24:51Z herbelin $ i*)
+(*i $Id: Notations.v 12271 2009-08-11 10:29:45Z herbelin $ i*)
(** These are the notations whose level and associativity are imposed by Coq *)
@@ -68,13 +68,13 @@ Reserved Notation "{ x }" (at level 0, x at level 99).
(** Notations for sigma-types or subsets *)
Reserved Notation "{ x | P }" (at level 0, x at level 99).
-Reserved Notation "{ x | P & Q }" (at level 0, x at level 99).
+Reserved Notation "{ x | P & Q }" (at level 0, x at level 99).
Reserved Notation "{ x : A | P }" (at level 0, x at level 99).
-Reserved Notation "{ x : A | P & Q }" (at level 0, x at level 99).
+Reserved Notation "{ x : A | P & Q }" (at level 0, x at level 99).
-Reserved Notation "{ x : A & P }" (at level 0, x at level 99).
-Reserved Notation "{ x : A & P & Q }" (at level 0, x at level 99).
+Reserved Notation "{ x : A & P }" (at level 0, x at level 99).
+Reserved Notation "{ x : A & P & Q }" (at level 0, x at level 99).
Delimit Scope type_scope with type.
Delimit Scope core_scope with core.
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 2d7e2159..48b4568d 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Tactics.v 11741 2009-01-03 14:34:39Z herbelin $ i*)
+(*i $Id: Tactics.v 13198 2010-06-25 22:36:20Z letouzey $ i*)
Require Import Notations.
Require Import Logic.
@@ -174,3 +174,20 @@ Tactic Notation "now" tactic(t) := t; easy.
(** A tactic to document or check what is proved at some point of a script *)
Ltac now_show c := change c.
+
+(** Clear an hypothesis and its dependencies *)
+
+Tactic Notation "clear" "dependent" hyp(h) :=
+ let rec depclear h :=
+ clear h ||
+ match goal with
+ | H : context [ h ] |- _ => depclear H; depclear h
+ end ||
+ fail "hypothesis to clear is used in the conclusion (maybe indirectly)"
+ in depclear h.
+
+(** Revert an hypothesis and its dependencies :
+ this is actually generalize dependent... *)
+
+Tactic Notation "revert" "dependent" hyp(h) :=
+ generalize dependent h.
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index a72283d9..c015854e 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: List.v 10999 2008-05-27 15:55:22Z letouzey $ i*)
+(*i $Id: List.v 12446 2009-10-29 21:43:06Z glondu $ i*)
Require Import Le Gt Minus Min Bool.
@@ -1081,11 +1081,11 @@ Section Map.
(** [flat_map] *)
- Fixpoint flat_map (f:A -> list B) (l:list A) {struct l} :
- list B :=
+ Definition flat_map (f:A -> list B) :=
+ fix flat_map (l:list A) {struct l} : list B :=
match l with
| nil => nil
- | cons x t => (f x)++(flat_map f t)
+ | cons x t => (f x)++(flat_map t)
end.
Lemma in_flat_map : forall (f:A->list B)(l:list A)(y:B),
diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v
index 21f2513f..f01cbbc5 100644
--- a/theories/Numbers/Rational/BigQ/BigQ.v
+++ b/theories/Numbers/Rational/BigQ/BigQ.v
@@ -8,7 +8,7 @@
(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
(************************************************************************)
-(*i $Id: BigQ.v 11208 2008-07-04 16:57:46Z letouzey $ i*)
+(*i $Id: BigQ.v 12509 2009-11-12 15:52:50Z letouzey $ i*)
Require Import Field Qfield BigN BigZ QSig QMake.
@@ -44,6 +44,11 @@ Delimit Scope bigQ_scope with bigQ.
Bind Scope bigQ_scope with bigQ.
Bind Scope bigQ_scope with BigQ.t.
+(* Allow nice printing of rational numerals, either as (Qz 1234)
+ or as (Qq 1234 5678) *)
+Arguments Scope BigQ.Qz [bigZ_scope].
+Arguments Scope BigQ.Qq [bigZ_scope bigN_scope].
+
Infix "+" := BigQ.add : bigQ_scope.
Infix "-" := BigQ.sub : bigQ_scope.
Notation "- x" := (BigQ.opp x) : bigQ_scope.
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index 78cf2892..0b6d1cfe 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: QArith_base.v 11301 2008-08-04 19:41:18Z herbelin $ i*)
+(*i $Id: QArith_base.v 13215 2010-06-29 09:31:45Z letouzey $ i*)
Require Export ZArith.
Require Export ZArithRing.
@@ -157,16 +157,15 @@ Qed.
(** We now consider [Q] seen as a setoid. *)
-Definition Q_Setoid : Setoid_Theory Q Qeq.
-Proof.
- split; red; unfold Qeq in |- *; auto; apply Qeq_trans.
-Qed.
+Add Relation Q Qeq
+ reflexivity proved by Qeq_refl
+ symmetry proved by Qeq_sym
+ transitivity proved by Qeq_trans
+as Q_Setoid.
-Add Setoid Q Qeq Q_Setoid as Qsetoid.
-
-Hint Resolve (Seq_refl Q Qeq Q_Setoid): qarith.
-Hint Resolve (Seq_sym Q Qeq Q_Setoid): qarith.
-Hint Resolve (Seq_trans Q Qeq Q_Setoid): qarith.
+Hint Resolve Qeq_refl : qarith.
+Hint Resolve Qeq_sym : qarith.
+Hint Resolve Qeq_trans : qarith.
Theorem Qnot_eq_sym : forall x y, ~x == y -> ~y == x.
Proof.
@@ -633,8 +632,15 @@ Proof.
unfold Qle, Qlt, Qeq; intros; apply Zle_lt_or_eq; auto.
Qed.
+(** These hints were meant to be added to the qarith database,
+ but a typo prevented that. This will be fixed in 8.3.
+ Concerning 8.2, for maximal compatibility , we
+ leave them in a separate database, in order to preserve
+ the strength of both [auto with qarith] and [auto with *].
+ (see bug #2346). *)
+
Hint Resolve Qle_not_lt Qlt_not_le Qnot_le_lt Qnot_lt_le
- Qlt_le_weak Qlt_not_eq Qle_antisym Qle_refl: qartih.
+ Qlt_le_weak Qlt_not_eq Qle_antisym Qle_refl: qarith_extra.
(** Some decidability results about orders. *)
diff --git a/theories/ZArith/Zbool.v b/theories/ZArith/Zbool.v
index 71befa4a..34771897 100644
--- a/theories/ZArith/Zbool.v
+++ b/theories/ZArith/Zbool.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: Zbool.v 11208 2008-07-04 16:57:46Z letouzey $ *)
+(* $Id: Zbool.v 12271 2009-08-11 10:29:45Z herbelin $ *)
Require Import BinInt.
Require Import Zeven.
@@ -18,9 +18,9 @@ Require Import Sumbool.
Unset Boxed Definitions.
Open Local Scope Z_scope.
-(** * Boolean operations from decidabilty of order *)
+(** * Boolean operations from decidability of order *)
(** The decidability of equality and order relations over
- type [Z] give some boolean functions with the adequate specification. *)
+ type [Z] gives some boolean functions with the adequate specification. *)
Definition Z_lt_ge_bool (x y:Z) := bool_of_sumbool (Z_lt_ge_dec x y).
Definition Z_ge_lt_bool (x y:Z) := bool_of_sumbool (Z_ge_lt_dec x y).
diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v
index 425aa83b..73808f92 100644
--- a/theories/ZArith/Zorder.v
+++ b/theories/ZArith/Zorder.v
@@ -5,7 +5,7 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Zorder.v 10291 2007-11-06 02:18:53Z letouzey $ i*)
+(*i $Id: Zorder.v 12888 2010-03-28 19:35:03Z herbelin $ i*)
(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *)
@@ -1025,3 +1025,5 @@ Qed.
(** For compatibility *)
Notation Zlt_O_minus_lt := Zlt_0_minus_lt (only parsing).
+Notation Zle_gt_succ := Zlt_gt_succ (only parsing).
+Notation Zle_succ_gt := Zlt_succ_gt (only parsing).
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index eb3a19fa..3ca1e7d3 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coq_makefile.ml4 12176 2009-06-09 09:44:40Z notin $ *)
+(* $Id: coq_makefile.ml4 12470 2009-11-05 15:50:20Z notin $ *)
(* créer un Makefile pour un développement Coq automatiquement *)
@@ -163,7 +163,7 @@ let install_include_by_root var files (_,inc_r) =
let ldir = List.assoc "." (List.map (fun (p,l,_) -> (p,l)) inc_r) in
let pdir = physical_dir_of_logical_dir ldir in
printf "\t(for i in $(%s); do \\\n" var;
- printf "\t install -D $$i $(COQLIB)/user-contrib/%s/$$i; \\\n" pdir;
+ printf "\t install -d `dirname $(COQLIB)/user-contrib/%s/$$i`; \\\n\t install $$i $(COQLIB)/user-contrib/%s/$$i; \\\n" pdir pdir;
printf "\t done)\n"
with Not_found ->
(* Files in the scope of a -R option (assuming they are disjoint) *)
@@ -172,12 +172,12 @@ let install_include_by_root var files (_,inc_r) =
begin
let pdir' = physical_dir_of_logical_dir ldir in
printf "\t(cd %s; for i in $(%s%d); do \\\n" pdir var i;
- printf "\t install -D $$i $(COQLIB)/user-contrib/%s/$$i; \\\n" pdir';
+ printf "\t install -d `dirname $(COQLIB)/user-contrib/%s/$$i`; \\\n\t install $$i $(COQLIB)/user-contrib/%s/$$i; \\\n" pdir' pdir';
printf "\t done)\n"
end) inc_r;
(* Files not in the scope of a -R option *)
printf "\t(for i in $(%s0); do \\\n" var;
- printf "\t install -D $$i $(COQLIB)/user-contrib/$(INSTALLDEFAULTROOT)/$$i; \\\n";
+ printf "\t install -d `dirname $(COQLIB)/user-contrib/$(INSTALLDEFAULTROOT)/$$i`; \\\n\t install $$i $(COQLIB)/user-contrib/$(INSTALLDEFAULTROOT)/$$i; \\\n";
printf "\t done)\n"
let install (vfiles,mlfiles,_,sds) inc =
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 4febe9d1..91a7e6d0 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coqdep.ml 11749 2009-01-05 14:01:04Z notin $ *)
+(* $Id: coqdep.ml 12916 2010-04-10 15:18:17Z herbelin $ *)
open Printf
open Coqdep_lexer
@@ -60,7 +60,9 @@ let safe_hash_add clq q (k,v) =
(k1,l1)::cltl when k=k1 -> (k1,v::l1)::cltl
| cl::cltl -> cl::add_clash cltl
| [] -> [(k,[v;v2])] in
- clq := add_clash !clq
+ clq := add_clash !clq;
+ (* overwrite previous bindings, as coqc does *)
+ Hashtbl.add q k v
with Not_found -> Hashtbl.add q k v
(* Files found in the loadpaths *)
@@ -167,6 +169,37 @@ let cut_prefix p s =
let ls = String.length s in
if ls >= lp && String.sub s 0 lp = p then String.sub s lp (ls - lp) else s
+(* Makefile's escaping rules are awful: $ is escaped by doubling and
+ other special characters are escaped by backslash prefixing while
+ backslashes themselves must be escaped only if part of a sequence
+ followed by a special character (i.e. in case of ambiguity with a
+ use of it as escaping character). Moreover (even if not crucial)
+ it is apparently not possible to directly escape ';' and leading '\t'. *)
+
+let escape =
+ let s' = Buffer.create 10 in
+ fun s ->
+ Buffer.clear s';
+ for i = 0 to String.length s - 1 do
+ let c = s.[i] in
+ if c = ' ' or c = '#' or c = ':' (* separators and comments *)
+ or c = '%' (* pattern *)
+ or c = '?' or c = '[' or c = ']' or c = '*' (* expansion in filenames *)
+ or i=0 && c = '~' && (String.length s = 1 || s.[1] = '/' ||
+ 'A' <= s.[1] && s.[1] <= 'Z' ||
+ 'a' <= s.[1] && s.[1] <= 'z') (* homedir expansion *)
+ then begin
+ let j = ref (i-1) in
+ while !j >= 0 && s.[!j] = '\\' do
+ Buffer.add_char s' '\\'; decr j (* escape all preceding '\' *)
+ done;
+ Buffer.add_char s' '\\';
+ end;
+ if c = '$' then Buffer.add_char s' '$';
+ Buffer.add_char s' c
+ done;
+ Buffer.contents s'
+
let canonize f =
let f' = absolute_dir (Filename.dirname f) // Filename.basename f in
match List.filter (fun (_,full) -> f' = full) !vAccu with
@@ -423,6 +456,11 @@ let add_coqlib_known phys_dir log_dir f =
Hashtbl.add coqlibKnown [basename] ();
Hashtbl.add coqlibKnown name ()
+let rec suffixes = function
+ | [] -> assert false
+ | [name] -> [[name]]
+ | dir::suffix as l -> l::suffixes suffix
+
let add_known phys_dir log_dir f =
if (Filename.check_suffix f ".ml" || Filename.check_suffix f ".mli" || Filename.check_suffix f ".ml4") then
let basename = make_ml_module_name f in
@@ -431,7 +469,7 @@ let add_known phys_dir log_dir f =
let basename = Filename.chop_suffix f ".v" in
let name = log_dir@[basename] in
let file = phys_dir//basename in
- let paths = [name;[basename]] in
+ let paths = suffixes name in
List.iter
(fun n -> safe_hash_add clash_v vKnown (n,file)) paths
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index c4a1a76f..b29e0734 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -7,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: pretty.mll 12187 2009-06-13 19:36:59Z msozeau $ i*)
+(*i $Id: pretty.mll 12908 2010-04-09 08:54:04Z herbelin $ i*)
(*s Utility functions for the scanners *)
@@ -126,7 +126,7 @@
Str.regexp "[ \t]*(\\*\\*[ \t]+printing[ \t]+\\([^ \t]+\\)"
let printing_token_re =
Str.regexp
- "[ \t]*\\(\\(%\\([^%]*\\)%\\)\\|\\(\\$[^$]*\\$\\)\\)?[ \t]*\\(#\\(\\([^#]\\|&#\\)*\\)#\\)?"
+ "[ \t]*\\(\\(%\\([^%]*\\)%\\)\\|\\(\\$[^$]*\\$\\)\\)?[ \t]*\\(#\\(\\(&#\\|[^#]\\)*\\)#\\)?"
let add_printing_token toks pps =
try
@@ -731,6 +731,9 @@ and body = parse
| token_no_brackets
{ let s = lexeme lexbuf in
symbol lexbuf s; body lexbuf }
+ | ".."
+ { Output.char '.'; Output.char '.';
+ body lexbuf }
| _ { let c = lexeme_char lexbuf 0 in
Output.char c;
body lexbuf }
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 6a75b99c..821a73f7 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: metasyntax.ml 11786 2009-01-14 13:07:34Z herbelin $ *)
+(* $Id: metasyntax.ml 12882 2010-03-23 22:34:38Z herbelin $ *)
open Pp
open Util
@@ -266,16 +266,18 @@ let split_notation_string str =
(* Interpret notations with a recursive component *)
-let rec find_pattern xl = function
- | Break n as x :: l, Break n' :: l' when n=n' ->
- find_pattern (x::xl) (l,l')
+let out_nt = function NonTerminal x -> x | _ -> assert false
+
+let rec find_pattern nt xl = function
+ | Break n as x :: l, Break n' :: l' when n=n' ->
+ find_pattern nt (x::xl) (l,l')
| Terminal s as x :: l, Terminal s' :: l' when s = s' ->
- find_pattern (x::xl) (l,l')
- | [NonTerminal x], NonTerminal x' :: l' ->
- (x,x',xl),l'
- | [NonTerminal _], Terminal s :: _ | Terminal s :: _, _ ->
+ find_pattern nt (x::xl) (l,l')
+ | [], NonTerminal x' :: l' ->
+ (out_nt nt,x',List.rev xl),l'
+ | [], Terminal s :: _ | Terminal s :: _, _ ->
error ("The token "^s^" occurs on one side of \"..\" but not on the other side.")
- | [NonTerminal _], Break s :: _ | Break s :: _, _ ->
+ | [], Break s :: _ | Break s :: _, _ ->
error ("A break occurs on one side of \"..\" but not on the other side.")
| ((SProdList _ | NonTerminal _) :: _ | []), _ ->
error ("The special symbol \"..\" must occur in a configuration of the form\n\"x symbs .. symbs y\".")
@@ -283,7 +285,8 @@ let rec find_pattern xl = function
let rec interp_list_parser hd = function
| [] -> [], [], List.rev hd
| NonTerminal id :: tl when id = ldots_var ->
- let ((x,y,sl),tl') = find_pattern [] (hd,tl) in
+ let hd = List.rev hd in
+ let ((x,y,sl),tl') = find_pattern (List.hd hd) [] (List.tl hd,tl) in
let yl,xl,tl'' = interp_list_parser [] tl' in
(* We remember each pair of variable denoting a recursive part to *)
(* remove the second copy of it afterwards *)
@@ -299,6 +302,7 @@ let rec interp_list_parser hd = function
yl, xl, List.rev_append hd tl'
| SProdList _ :: _ -> anomaly "Unexpected SProdList in interp_list_parser"
+
(* Find non-terminal tokens of notation *)
let unquote_notation_token s =
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 176f336b..b54700d3 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -11,7 +11,7 @@
* camlp4deps will not work for this file unless Makefile system enhanced.
*)
-(* $Id: mltop.ml4 11801 2009-01-18 20:11:41Z herbelin $ *)
+(* $Id: mltop.ml4 12341 2009-09-17 16:03:19Z glondu $ *)
open Util
open Pp
@@ -109,7 +109,7 @@ let dir_ml_load s =
* in this file, the Makefile dependency logic needs to be updated.
*)
let warn = Flags.is_verbose() in
- let _,gname = where_in_path ~warn !coq_mlpath_copy s in
+ let _,gname = find_file_in_path ~warn !coq_mlpath_copy s in
try
Dynlink.loadfile gname;
with | Dynlink.Error a ->
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index a1acd1d6..9d64f983 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: toplevel.ml 11784 2009-01-14 11:36:32Z herbelin $ *)
+(* $Id: toplevel.ml 12891 2010-03-30 11:40:02Z herbelin $ *)
open Pp
open Util
@@ -163,11 +163,10 @@ let print_location_in_file s inlibrary fname loc =
try
let (line, bol) = line_of_pos 1 0 0 in
close_in ic;
- hov 0
- (errstrm ++ str"File " ++ str ("\""^fname^"\"") ++ str"," ++ spc() ++
- hov 0 (str"line " ++ int line ++ str"," ++ spc() ++
- str"characters " ++
- Cerrors.print_loc (make_loc (bp-bol,ep-bol))) ++ str":") ++
+ hov 0 (* No line break so as to follow emacs error message format *)
+ (errstrm ++ str"File " ++ str ("\""^fname^"\"") ++
+ str", line " ++ int line ++ str", characters " ++
+ Cerrors.print_loc (make_loc (bp-bol,ep-bol))) ++ str":" ++
fnl ()
with e ->
(close_in ic;
@@ -316,7 +315,7 @@ let parse_to_dot =
let rec discard_to_dot () =
try
Gram.Entry.parse parse_to_dot top_buffer.tokens
- with Stdpp.Exc_located(_,Token.Error _) ->
+ with Stdpp.Exc_located(_,(Token.Error _|Lexer.Error _)) ->
discard_to_dot()
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 6a0acb52..385afbec 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: vernacentries.ml 12187 2009-06-13 19:36:59Z msozeau $ i*)
+(*i $Id: vernacentries.ml 12343 2009-09-17 17:02:03Z glondu $ i*)
(* Concrete syntax of the mathematical vernacular MV V2.6 *)
@@ -234,12 +234,8 @@ let dump_universes s =
(* "Locate" commands *)
let locate_file f =
- try
- let _,file = System.where_in_path ~warn:false (Library.get_load_paths ()) f in
- msgnl (str file)
- with Not_found ->
- msgnl (hov 0 (str"Can't find file" ++ spc () ++ str f ++ spc () ++
- str"on loadpath"))
+ let _,file = System.find_file_in_path ~warn:false (Library.get_load_paths ()) f in
+ msgnl (str file)
let msg_found_library = function
| Library.LibLoaded, fulldir, file ->