diff options
Diffstat (limited to 'toplevel')
49 files changed, 122 insertions, 115 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 6064c3d4..16ceffed 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: auto_ind_decl.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: auto_ind_decl.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) (* This file is about the automatic generation of schemes about decidable equality, created by Vincent Siles, Oct 2007 *) diff --git a/toplevel/auto_ind_decl.mli b/toplevel/auto_ind_decl.mli index fc7aecad..c791da28 100644 --- a/toplevel/auto_ind_decl.mli +++ b/toplevel/auto_ind_decl.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml index 62a97281..4a67ede4 100644 --- a/toplevel/autoinstance.ml +++ b/toplevel/autoinstance.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -191,7 +191,7 @@ let declare_class_instance gr ctx params = let ident = make_instance_ident gr in let cl = Typeclasses.class_info gr in let (def,typ) = Typeclasses.instance_constructor cl params in - let (def,typ) = it_mkLambda_or_LetIn def ctx, it_mkProd_or_LetIn typ ctx in + let (def,typ) = it_mkLambda_or_LetIn (Option.get def) ctx, it_mkProd_or_LetIn typ ctx in let def = deep_refresh_universes def in let typ = deep_refresh_universes typ in let ce = Entries.DefinitionEntry diff --git a/toplevel/autoinstance.mli b/toplevel/autoinstance.mli index 9478aa16..b9b1e3c2 100644 --- a/toplevel/autoinstance.mli +++ b/toplevel/autoinstance.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index 3bba0605..86057b4b 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: cerrors.ml 13639 2010-11-16 15:36:01Z glondu $ *) +(* $Id: cerrors.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Pp open Util diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli index 31e0e04f..e1f7c035 100644 --- a/toplevel/cerrors.mli +++ b/toplevel/cerrors.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: cerrors.mli 13431 2010-09-18 08:15:29Z herbelin $ i*) +(*i $Id: cerrors.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Pp diff --git a/toplevel/class.ml b/toplevel/class.ml index 0ee9dd19..09ce84e0 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: class.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: class.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Util open Pp diff --git a/toplevel/class.mli b/toplevel/class.mli index 057d85ac..b05f38e7 100644 --- a/toplevel/class.mli +++ b/toplevel/class.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: class.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: class.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Names diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 2d8aabfc..28c1ab75 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -1,13 +1,13 @@ (* -*- compile-command: "make -C .. bin/coqtop.byte" -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: classes.ml 13516 2010-10-07 19:09:38Z msozeau $ i*) +(*i $Id: classes.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Names @@ -245,8 +245,8 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props in let app, ty_constr = instance_constructor k subst in let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in - let term = Termops.it_mkLambda_or_LetIn app (ctx' @ ctx) in - term, termtype + let term = Termops.it_mkLambda_or_LetIn (Option.get app) (ctx' @ ctx) in + term, termtype | Inr (def, subst) -> let termtype = it_mkProd_or_LetIn cty ctx in let term = Termops.it_mkLambda_or_LetIn def ctx in diff --git a/toplevel/classes.mli b/toplevel/classes.mli index 61670e0d..69e4dd8b 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: classes.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: classes.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Names diff --git a/toplevel/command.ml b/toplevel/command.ml index 2d0cdea6..1112ac6d 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: command.ml 13672 2010-12-03 20:05:46Z herbelin $ *) +(* $Id: command.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Pp open Util diff --git a/toplevel/command.mli b/toplevel/command.mli index f5996905..af89b59a 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: command.mli 13332 2010-07-26 22:12:43Z msozeau $ i*) +(*i $Id: command.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Util diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index bce38128..210507e1 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqinit.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: coqinit.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Pp open System diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli index c2a535dd..c0f59a56 100644 --- a/toplevel/coqinit.mli +++ b/toplevel/coqinit.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: coqinit.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: coqinit.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (* Initialization. *) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index f05509a4..7887a060 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqtop.ml 13358 2010-07-29 23:10:17Z herbelin $ *) +(* $Id: coqtop.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Pp open Util diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index e80b3252..ef730915 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: coqtop.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: coqtop.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (* The Coq main module. The following function [start] will parse the command line, print the banner, initialize the load path, load the input diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 6f74c526..58122e11 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: discharge.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: discharge.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Names open Util @@ -67,13 +67,20 @@ let abstract_inductive hyps nparams inds = inds' in (params',ind'') +let refresh_polymorphic_type_of_inductive (_,mip) = + match mip.mind_arity with + | Monomorphic s -> + s.mind_user_arity + | Polymorphic ar -> + let ctx = List.rev mip.mind_arity_ctxt in + mkArity (List.rev ctx,Termops.new_Type_sort()) let process_inductive sechyps modlist mib = let nparams = mib.mind_nparams in let inds = array_map_to_list (fun mip -> - let arity = expmod_constr modlist (Termops.refresh_universes_strict (Inductive.type_of_inductive (Global.env()) (mib,mip))) in + let arity = expmod_constr modlist (refresh_polymorphic_type_of_inductive (mib,mip)) in let lc = Array.map (expmod_constr modlist) mip.mind_user_lc in (mip.mind_typename, arity, diff --git a/toplevel/discharge.mli b/toplevel/discharge.mli index dda4c5d7..f881e8a2 100644 --- a/toplevel/discharge.mli +++ b/toplevel/discharge.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: discharge.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: discharge.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) open Sign open Cooking diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 99ca9879..62d19bea 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: himsg.ml 13465 2010-09-24 22:23:07Z herbelin $ *) +(* $Id: himsg.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Pp open Util diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli index a916e87b..e12e445c 100644 --- a/toplevel/himsg.mli +++ b/toplevel/himsg.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: himsg.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: himsg.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Pp diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index c2d5f31d..53c3bcea 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ind_tables.ml 13392 2010-09-02 12:11:15Z vsiles $ i*) +(*i $Id: ind_tables.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) (* File created by Vincent Siles, Oct 2007, extended into a generic support for generation of inductive schemes by Hugo Herbelin, Nov 2009 *) diff --git a/toplevel/ind_tables.mli b/toplevel/ind_tables.mli index 1374a0a4..e6f5e77a 100644 --- a/toplevel/ind_tables.mli +++ b/toplevel/ind_tables.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index 9031d8a3..3596085f 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: indschemes.ml 13396 2010-09-02 16:52:15Z vsiles $ *) +(* $Id: indschemes.ml 14641 2011-11-06 11:59:10Z herbelin $ *) (* Created by Hugo Herbelin from contents related to inductive schemes initially developed by Christine Paulin (induction schemes), Vincent @@ -295,34 +295,34 @@ requested *) | (None,t)::q -> let l1,l2 = split_scheme q in - let names inds recs x y z = + let names inds recs isdep y z = let ind = smart_global_inductive y in - let sort_of_ind = Retyping.get_sort_family_of env Evd.empty (mkInd ind) in + let sort_of_ind = inductive_sort_family (snd (lookup_mind_specif env ind)) in let z' = family_of_sort (interp_sort z) in let suffix = ( match sort_of_ind with | InProp -> - if x then (match z' with - | InProp -> inds ^ "_nodep" - | InSet -> recs ^ "_nodep" - | InType -> recs ^ "t_nodep") + if isdep then (match z' with + | InProp -> inds ^ "_dep" + | InSet -> recs ^ "_dep" + | InType -> recs ^ "t_dep") else ( match z' with | InProp -> inds | InSet -> recs | InType -> recs ^ "t" ) | _ -> - if x then (match z' with + if isdep then (match z' with | InProp -> inds | InSet -> recs | InType -> recs ^ "t" ) else (match z' with - | InProp -> inds ^ "_dep" - | InSet -> recs ^ "_dep" - | InType -> recs ^ "t_dep") + | InProp -> inds ^ "_nodep" + | InSet -> recs ^ "_nodep" + | InType -> recs ^ "t_nodep") ) in let newid = add_suffix (basename_of_global (IndRef ind)) suffix in let newref = (dummy_loc,newid) in - ((newref,x,ind,z)::l1),l2 + ((newref,isdep,ind,z)::l1),l2 in match t with | CaseScheme (x,y,z) -> names "_case" "_case" x y z diff --git a/toplevel/indschemes.mli b/toplevel/indschemes.mli index f763e182..707b9e00 100644 --- a/toplevel/indschemes.mli +++ b/toplevel/indschemes.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: indschemes.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: indschemes.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Util diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml index 7af5d0aa..8ef82105 100644 --- a/toplevel/lemmas.ml +++ b/toplevel/lemmas.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: lemmas.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: lemmas.ml 14641 2011-11-06 11:59:10Z herbelin $ *) (* Created by Hugo Herbelin from contents related to lemma proofs in file command.ml, Aug 2009 *) diff --git a/toplevel/lemmas.mli b/toplevel/lemmas.mli index 5327f63f..0e8eaac2 100644 --- a/toplevel/lemmas.mli +++ b/toplevel/lemmas.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: lemmas.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: lemmas.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Names diff --git a/toplevel/libtypes.ml b/toplevel/libtypes.ml index 41680036..27e19bd8 100644 --- a/toplevel/libtypes.ml +++ b/toplevel/libtypes.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/toplevel/libtypes.mli b/toplevel/libtypes.mli index f3839ec1..03329592 100644 --- a/toplevel/libtypes.mli +++ b/toplevel/libtypes.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index c1663685..0adae08a 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: metasyntax.ml 13690 2010-12-06 16:15:54Z glondu $ *) +(* $Id: metasyntax.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Pp open Flags diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli index d8dd0d52..2c4e29bb 100644 --- a/toplevel/metasyntax.mli +++ b/toplevel/metasyntax.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: metasyntax.mli 13328 2010-07-26 11:05:30Z herbelin $ i*) +(*i $Id: metasyntax.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Util diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index e8c06d13..59bc01d0 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -11,7 +11,7 @@ * camlp4deps will not work for this file unless Makefile system enhanced. *) -(* $Id: mltop.ml4 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: mltop.ml4 14641 2011-11-06 11:59:10Z herbelin $ *) open Util open Pp diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli index 12b6f78f..ae562bd2 100644 --- a/toplevel/mltop.mli +++ b/toplevel/mltop.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: mltop.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: mltop.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (* If there is a toplevel under Coq, it is described by the following record. *) diff --git a/toplevel/record.ml b/toplevel/record.ml index 773d3390..ee9b8d66 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: record.ml 13492 2010-10-04 21:20:01Z herbelin $ *) +(* $Id: record.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Pp open Util @@ -137,7 +137,10 @@ let subst_projection fid l c = match List.nth l (k-depth-2) with | Projection t -> lift depth t | NoProjection (Name id) -> bad_projs := id :: !bad_projs; mkRel k - | NoProjection Anonymous -> assert false + | NoProjection Anonymous -> + errorlabstrm "" (str "Field " ++ pr_id fid ++ + str " depends on the " ++ str (ordinal (k-depth-1)) ++ str + " field which has no name.") else mkRel (k-lv) | _ -> map_constr_with_binders succ substrec depth c diff --git a/toplevel/record.mli b/toplevel/record.mli index ea4a3b7e..44b34550 100644 --- a/toplevel/record.mli +++ b/toplevel/record.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: record.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: record.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Names diff --git a/toplevel/search.ml b/toplevel/search.ml index 574983cd..fd3024a4 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: search.ml 13853 2011-02-24 07:57:31Z glondu $ *) +(* $Id: search.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Pp open Util diff --git a/toplevel/search.mli b/toplevel/search.mli index a73052f2..6a85a12f 100644 --- a/toplevel/search.mli +++ b/toplevel/search.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: search.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: search.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) open Pp open Names diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index 299214f0..9954ff56 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: toplevel.ml 13668 2010-12-02 17:43:59Z herbelin $ *) +(* $Id: toplevel.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Pp open Util diff --git a/toplevel/toplevel.mli b/toplevel/toplevel.mli index a614c1da..022a6541 100644 --- a/toplevel/toplevel.mli +++ b/toplevel/toplevel.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: toplevel.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: toplevel.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Pp diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 22588f2c..0282f30a 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: usage.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: usage.ml 14641 2011-11-06 11:59:10Z herbelin $ *) let version () = Printf.printf "The Coq Proof Assistant, version %s (%s)\n" diff --git a/toplevel/usage.mli b/toplevel/usage.mli index 1167750b..721edccb 100644 --- a/toplevel/usage.mli +++ b/toplevel/usage.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: usage.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: usage.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*s Prints the version number on the standard output and exits (with 0). *) diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index afc5057e..a7aef93f 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: vernac.ml 13923 2011-03-21 16:25:20Z letouzey $ *) +(* $Id: vernac.ml 14641 2011-11-06 11:59:10Z herbelin $ *) (* Parsing of vernacular. *) diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index dc4d9e2f..54ce9244 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: vernac.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: vernac.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (* Parsing of vernacular. *) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 7710cb95..3be3c6db 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: vernacentries.ml 13922 2011-03-21 16:25:18Z letouzey $ i*) +(*i $Id: vernacentries.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) (* Concrete syntax of the mathematical vernacular MV V2.6 *) @@ -370,9 +370,6 @@ let vernac_exact_proof c = (strbrk "Command 'Proof ...' can only be used at the beginning of the proof.") let vernac_assumption kind l nl= - if Pfedit.refining () then - errorlabstrm "" - (str "Cannot declare an assumption while in proof editing mode."); let global = fst kind = Global in List.iter (fun (is_coe,(idl,c)) -> if Dumpglob.dump () then @@ -1113,12 +1110,12 @@ let vernac_print = function pp (Notation.pr_visibility (Constrextern.without_symbols pr_lrawconstr) s) | PrintAbout qid -> msg (print_about qid) | PrintImplicit qid -> msg (print_impargs qid) -(*spiwack: prints all the axioms and section variables used by a term *) | PrintAssumptions (o,r) -> + (* Prints all the axioms and section variables used by a term *) let cstr = constr_of_global (smart_global r) in - let nassumptions = Environ.assumptions (Conv_oracle.get_transp_state ()) - ~add_opaque:o cstr (Global.env ()) in - msg (Printer.pr_assumptionset (Global.env ()) nassumptions) + let st = Conv_oracle.get_transp_state () in + let nassums = Assumptions.assumptions st ~add_opaque:o cstr in + msg (Printer.pr_assumptionset (Global.env ()) nassums) let global_module r = let (loc,qid) = qualid_of_reference r in diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli index 10ed35a7..1cca3540 100644 --- a/toplevel/vernacentries.mli +++ b/toplevel/vernacentries.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: vernacentries.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: vernacentries.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Names diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 0d247189..31c46a54 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: vernacexpr.ml 13668 2010-12-02 17:43:59Z herbelin $ i*) +(*i $Id: vernacexpr.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) open Util open Names diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml index f3d2e7a5..e6fe9a4f 100644 --- a/toplevel/vernacinterp.ml +++ b/toplevel/vernacinterp.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: vernacinterp.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: vernacinterp.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Pp open Util diff --git a/toplevel/vernacinterp.mli b/toplevel/vernacinterp.mli index ce64188c..780e4e28 100644 --- a/toplevel/vernacinterp.mli +++ b/toplevel/vernacinterp.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: vernacinterp.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: vernacinterp.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Tacexpr diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 index 15caaddd..e380ae6f 100644 --- a/toplevel/whelp.ml4 +++ b/toplevel/whelp.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: whelp.ml4 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: whelp.ml4 14641 2011-11-06 11:59:10Z herbelin $ *) open Flags open Pp diff --git a/toplevel/whelp.mli b/toplevel/whelp.mli index 27c36239..75e9ad49 100644 --- a/toplevel/whelp.mli +++ b/toplevel/whelp.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: whelp.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: whelp.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (* Coq interface to the Whelp query engine developed at the University of Bologna *) |