diff options
author | 2011-12-25 13:24:00 +0100 | |
---|---|---|
committer | 2011-12-25 13:24:00 +0100 | |
commit | 48c05753a959be121af5c1712e8ad114b18874f6 (patch) | |
tree | 8ad1a16af591eb44dc8563e7d7a41748ecdfb9e7 /pretyping | |
parent | 5f43edb15fbe34bf1f31a7155e40896baa067796 (diff) | |
parent | 5fe4ac437bed43547b3695664974f492b55cb553 (diff) |
Merge commit 'upstream/8.3.pl3+dfsg'
Diffstat (limited to 'pretyping')
56 files changed, 180 insertions, 165 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 67bf7043..749101f7 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.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: cases.ml 13962 2011-04-06 17:00:45Z herbelin $ *) +(* $Id: cases.ml 14675 2011-11-17 22:19:34Z herbelin $ *) open Util open Names @@ -409,15 +409,14 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) = the first pattern type and forget about the others *) let typ,names = match typ with IsInd(t,_,names) -> t,Some names | NotInd(_,t) -> t,None in - let typ = + let tmtyp = try try_find_ind pb.env !(pb.evdref) typ names with Not_found -> NotInd (None,typ) in - let tomatch = ((current,typ),deps,dep) in - match typ with + match tmtyp with | NotInd (None,typ) -> let tm1 = List.map (fun eqn -> List.hd eqn.patterns) pb.mat in (match find_row_ind tm1 with - | None -> tomatch + | None -> (current,tmtyp) | Some (_,(ind,_)) -> let indt = inductive_template pb.evdref pb.env None ind in let current = @@ -429,9 +428,8 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) = (evd_comb2 (Coercion.inh_conv_coerce_to dummy_loc pb.env) pb.evdref (make_judge current typ) (mk_tycon_type indt)).uj_val in let sigma = !(pb.evdref) in - let typ = try_find_ind pb.env sigma indt names in - ((current,typ),deps,dep)) - | _ -> tomatch + (current,try_find_ind pb.env sigma indt names)) + | _ -> (current,tmtyp) let type_of_tomatch = function | IsInd (t,_,_) -> t @@ -875,22 +873,24 @@ let generalize_predicate (names,(nadep,_)) ny d tms ccl = let ccl = lift_predicate 1 ccl tms in regeneralize_index_predicate (ny+p+1) ccl tms -let rec extract_predicate l ccl = function - | Alias (deppat,nondeppat,_,_)::tms -> - let tms' = match kind_of_term nondeppat with - | Rel i -> replace_tomatch i deppat tms - | _ -> (* initial terms are not dependent *) tms in - extract_predicate l ccl tms' - | Abstract d'::tms -> - let d' = map_rel_declaration (lift (List.length l)) d' in - substl l (mkProd_or_LetIn d' (extract_predicate [] ccl tms)) +let rec extract_predicate ccl = function + | Alias (deppat,nondeppat,_,_)::tms -> + (* substitution already done in build_branch *) + extract_predicate ccl tms + | Abstract d::tms -> + mkProd_or_LetIn d (extract_predicate ccl tms) | Pushed ((cur,NotInd _),_,(dep,_))::tms -> - extract_predicate (if dep<>Anonymous then cur::l else l) ccl tms + let tms = if dep<>Anonymous then lift_tomatch_stack 1 tms else tms in + let pred = extract_predicate ccl tms in + if dep<>Anonymous then subst1 cur pred else pred | Pushed ((cur,IsInd (_,IndType(_,realargs),_)),_,(dep,_))::tms -> - let l = List.rev realargs@l in - extract_predicate (if dep<>Anonymous then cur::l else l) ccl tms + let realargs = List.rev realargs in + let k = if dep<>Anonymous then 1 else 0 in + let tms = lift_tomatch_stack (List.length realargs + k) tms in + let pred = extract_predicate ccl tms in + substl (if dep<>Anonymous then cur::realargs else realargs) pred | [] -> - substl l ccl + ccl let abstract_predicate env sigma indf cur (names,(nadep,_)) tms ccl = let sign = make_arity_signature env true indf in @@ -903,7 +903,7 @@ let abstract_predicate env sigma indf cur (names,(nadep,_)) tms ccl = | _ -> (* Initial case *) tms in let sign = List.map2 (fun na (_,c,t) -> (na,c,t)) (nadep::names) sign in let ccl = if nadep <> Anonymous then ccl else lift_predicate 1 ccl tms in - let pred = extract_predicate [] ccl tms in + let pred = extract_predicate ccl tms in it_mkLambda_or_LetIn_name env pred sign let known_dependent (_,dep) = (dep = KnownDep) @@ -982,14 +982,18 @@ let find_predicate loc env evdref p current (IndType (indf,realargs)) dep tms = (pred, whd_betaiota !evdref (applist (pred, realargs@[current])), new_Type ()) -let adjust_predicate_from_tomatch ((_,oldtyp),_,(nadep,_)) typ pb = +(* Take into account that a type has been discovered to be inductive, leading + to more dependencies in the predicate if the type has indices *) +let adjust_predicate_from_tomatch tomatch (current,typ as ct) pb = + let ((_,oldtyp),deps,((nadep,_) as dep)) = tomatch in match typ, oldtyp with | IsInd (_,_,names), NotInd _ -> let k = if nadep <> Anonymous then 2 else 1 in let n = List.length names in - { pb with pred = liftn_predicate n k pb.pred pb.tomatch } + { pb with pred = liftn_predicate n k pb.pred pb.tomatch }, + (ct,List.map (fun i -> if i >= k then i+n else i) deps,dep) | _ -> - pb + pb, (ct,deps,dep) (************************************************************************) (* Sorting equations by constructor *) @@ -1105,6 +1109,10 @@ let build_branch current deps (realnames,dep) pb arsign eqns const_info = (* into "Gamma; typs; curalias |- tms" *) let tomatch = lift_tomatch_stack const_info.cs_nargs pb.tomatch in + let tomatch = match kind_of_term current with + | Rel i -> replace_tomatch (i+const_info.cs_nargs) ci tomatch + | _ -> (* non-rel initial term *) tomatch in + let pred_is_not_dep = noccur_predicate_between 1 (List.length realnames + 1) pb.pred tomatch in @@ -1171,20 +1179,22 @@ let rec compile pb = | (Abstract d)::rest -> compile_generalization pb d rest | [] -> build_leaf pb +(* Case splitting *) and match_current pb tomatch = - let ((current,typ),deps,dep as ct) = adjust_tomatch_to_pattern pb tomatch in - let pb = adjust_predicate_from_tomatch tomatch typ pb in + let tm = adjust_tomatch_to_pattern pb tomatch in + let pb,tomatch = adjust_predicate_from_tomatch tomatch tm pb in + let ((current,typ),deps,dep) = tomatch in match typ with | NotInd (_,typ) -> check_all_variables typ pb.mat; - compile (shift_problem ct pb) + compile (shift_problem tomatch pb) | IsInd (_,(IndType(indf,realargs) as indt),names) -> let mind,_ = dest_ind_family indf in let cstrs = get_constructors pb.env indf in let arsign, _ = get_arity pb.env indf in let eqns,onlydflt = group_equations pb mind current cstrs pb.mat in if (Array.length cstrs <> 0 or pb.mat <> []) & onlydflt then - compile (shift_problem ct pb) + compile (shift_problem tomatch pb) else let _constraints = Array.map (solve_constraints indt) cstrs in @@ -1220,21 +1230,11 @@ and compile_generalization pb d rest = { uj_val = mkLambda_or_LetIn d j.uj_val; uj_type = mkProd_or_LetIn d j.uj_type } -and compile_alias pb (deppat,nondeppat,d,t) rest = +and compile_alias pb aliases rest = let history = simplify_history pb.history in - let sign, newenv, mat = - insert_aliases pb.env !(pb.evdref) (deppat,nondeppat,d,t) pb.mat in + let sign, newenv, mat = insert_aliases pb.env !(pb.evdref) aliases pb.mat in let n = List.length sign in - - (* We had Gamma1; x:current; Gamma2 |- tomatch(x) and we rebind x to get *) - (* Gamma1; x:current; Gamma2; typs; x':=curalias |- tomatch(x') *) let tomatch = lift_tomatch_stack n rest in - let tomatch = match kind_of_term nondeppat with - | Rel i -> - if n = 1 then regeneralize_index_tomatch (i+n) tomatch - else replace_tomatch i deppat tomatch - | _ -> (* initial terms are not dependent *) tomatch in - let pb = {pb with env = newenv; @@ -1395,7 +1395,10 @@ let build_tycon loc env tycon_env subst tycon extenv evdref t = e_new_evar evdref env ~src:(loc,ImpossibleCase) (new_Type ()) in lift (n'-n) impossible_case_type | Some t -> abstract_tycon loc tycon_env evdref subst tycon extenv t in - get_judgment_of extenv !evdref t + try get_judgment_of extenv !evdref t + with Not_found | Anomaly _ -> + (* Quick workaround to acknowledge failure to build a well-typed pred *) + error "Unable to infer a well-typed return clause." (* For a multiple pattern-matching problem Xi on t1..tn with return * type T, [build_inversion_problem Gamma Sigma (t1..tn) T] builds a return diff --git a/pretyping/cases.mli b/pretyping/cases.mli index 7bc635fb..2711276a 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.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: cases.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: cases.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Util diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index ec71159b..802f9c58 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.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: cbv.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: cbv.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Util open Pp diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli index 5486b064..e66e6dc6 100644 --- a/pretyping/cbv.mli +++ b/pretyping/cbv.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: cbv.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: cbv.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Names diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 17f18a9b..504d01af 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.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: classops.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: classops.ml 14776 2011-12-07 17:54:28Z herbelin $ *) open Util open Pp @@ -369,8 +369,8 @@ let load_coercion _ o = then cache_coercion o -let open_coercion _ o = - if not +let open_coercion i o = + if i = 1 && not (!automatically_import_coercions || Flags.version_less_or_equal Flags.V8_2) then cache_coercion o diff --git a/pretyping/classops.mli b/pretyping/classops.mli index f905e392..964b44a0 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.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: classops.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: classops.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Names diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index b9fd307c..abfef8d4 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.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: clenv.ml 13902 2011-03-10 15:50:24Z msozeau $ *) +(* $Id: clenv.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Pp open Util diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli index b50e313c..6fbb668b 100644 --- a/pretyping/clenv.mli +++ b/pretyping/clenv.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: clenv.mli 13332 2010-07-26 22:12:43Z msozeau $ i*) +(*i $Id: clenv.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Util diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index dd099aa1..d0f20615 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -1,11 +1,11 @@ (************************************************************************) (* 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: coercion.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: coercion.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Util open Names diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli index 00848dac..6ad1023e 100644 --- a/pretyping/coercion.mli +++ b/pretyping/coercion.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: coercion.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: coercion.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Util diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index e435484e..14e72807 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.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: detyping.ml 13329 2010-07-26 11:05:39Z herbelin $ *) +(* $Id: detyping.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Pp open Util @@ -467,7 +467,7 @@ and share_names isgoal n l avoid env c t = let b = detype isgoal avoid env b in let id = next_name_away na avoid in let avoid = id::avoid and env = add_name (Name id) env in - share_names isgoal n ((Name id,Explicit,Some b,t')::l) avoid env c t + share_names isgoal n ((Name id,Explicit,Some b,t')::l) avoid env c (lift 1 t) (* Only if built with the f/n notation or w/o let-expansion in types *) | _, LetIn (_,b,_,t) when n > 0 -> share_names isgoal n l avoid env c (subst1 b t) diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index cdb840b6..556b2477 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.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: detyping.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: detyping.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Util diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 51183be3..6d080016 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.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: evarconv.ml 13332 2010-07-26 22:12:43Z msozeau $ *) +(* $Id: evarconv.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Pp open Util diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index b0702038..50228d4e 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.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: evarconv.mli 13332 2010-07-26 22:12:43Z msozeau $ i*) +(*i $Id: evarconv.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Term diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 09ec8dda..b95b50b3 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.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: evarutil.ml 13332 2010-07-26 22:12:43Z msozeau $ *) +(* $Id: evarutil.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Util open Pp diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index d677b972..e29effc2 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.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: evarutil.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: evarutil.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Util diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 5d61e727..2db77837 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.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: evd.ml 13902 2011-03-10 15:50:24Z msozeau $ *) +(* $Id: evd.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Pp open Util diff --git a/pretyping/evd.mli b/pretyping/evd.mli index c68cfffe..8a903f1b 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.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: evd.mli 13902 2011-03-10 15:50:24Z msozeau $ i*) +(*i $Id: evd.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Util diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 927af594..edbab0a7 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.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: indrec.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: indrec.ml 14641 2011-11-06 11:59:10Z herbelin $ *) (* File initially created by Christine Paulin, 1996 *) diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli index 188ad74d..b2375c8f 100644 --- a/pretyping/indrec.mli +++ b/pretyping/indrec.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: indrec.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: indrec.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Names diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 85c865fa..6e54c170 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.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: inductiveops.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: inductiveops.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Util open Names diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 251c6b2e..e5759864 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.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: inductiveops.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: inductiveops.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) open Names open Term diff --git a/pretyping/matching.ml b/pretyping/matching.ml index 6ee67bf2..f0536f22 100644 --- a/pretyping/matching.ml +++ b/pretyping/matching.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: matching.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: matching.ml 14641 2011-11-06 11:59:10Z herbelin $ *) (*i*) open Util diff --git a/pretyping/matching.mli b/pretyping/matching.mli index 25863129..fc0e3feb 100644 --- a/pretyping/matching.mli +++ b/pretyping/matching.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: matching.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: matching.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Names diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml index 6e3e2f7c..45060511 100644 --- a/pretyping/namegen.ml +++ b/pretyping/namegen.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: namegen.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: namegen.ml 14641 2011-11-06 11:59:10Z herbelin $ *) (* Created from contents that was formerly in termops.ml and nameops.ml, Nov 2009 *) diff --git a/pretyping/namegen.mli b/pretyping/namegen.mli index 419624b8..f99ee3f6 100644 --- a/pretyping/namegen.mli +++ b/pretyping/namegen.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 *) (************************************************************************) -(* $Id: namegen.mli 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: namegen.mli 14641 2011-11-06 11:59:10Z herbelin $ *) open Names open Term diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index d1c4cfc1..83bfe9ea 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.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: pattern.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: pattern.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Util open Names diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli index fbc6bbaa..195fecfe 100644 --- a/pretyping/pattern.mli +++ b/pretyping/pattern.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: pattern.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: pattern.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Pp diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 6befdedc..688a25b9 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.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: pretype_errors.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: pretype_errors.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Util open Stdpp diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 496e16d2..d3e6ffea 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.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: pretype_errors.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: pretype_errors.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Pp diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index b8dc719b..a3b1dd18 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.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: pretyping.ml 13780 2011-01-07 16:37:57Z herbelin $ *) +(* $Id: pretyping.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Pp open Util diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 7d08026f..b94f9789 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.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: pretyping.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: pretyping.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Names diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index afb942fb..978dbeef 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.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: rawterm.ml 13329 2010-07-26 11:05:39Z herbelin $ *) +(* $Id: rawterm.ml 14641 2011-11-06 11:59:10Z herbelin $ *) (*i*) open Util diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index 39ff74a3..10156cec 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.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: rawterm.mli 13329 2010-07-26 11:05:39Z herbelin $ i*) +(*i $Id: rawterm.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Util diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 68ae9208..e8c6073e 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.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: recordops.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: recordops.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Util open Pp diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 78626854..b71c4969 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.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: recordops.mli 13447 2010-09-21 13:23:45Z letouzey $ i*) +(*i $Id: recordops.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Names diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 556134de..5af20551 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.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: reductionops.ml 13354 2010-07-29 16:44:45Z barras $ *) +(* $Id: reductionops.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Pp open Util diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index f557df00..95032bde 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.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: reductionops.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: reductionops.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Names diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index e4a85b84..7fb4f7ba 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.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: retyping.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: retyping.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Util open Term @@ -44,7 +44,7 @@ let type_of_var env id = with Not_found -> anomaly ("type_of: variable "^(string_of_id id)^" unbound") -let retype sigma = +let retype ?(polyprop=true) sigma = let rec type_of env cstr= match kind_of_term cstr with | Meta n -> @@ -129,7 +129,7 @@ let retype sigma = match kind_of_term c with | Ind ind -> let (_,mip) = lookup_mind_specif env ind in - Inductive.type_of_inductive_knowing_parameters env mip argtyps + Inductive.type_of_inductive_knowing_parameters ~polyprop env mip argtyps | Const cst -> let t = constant_type env cst in Typeops.type_of_constant_knowing_parameters env t argtyps @@ -140,8 +140,10 @@ let retype sigma = in type_of, sort_of, sort_family_of, type_of_global_reference_knowing_parameters -let get_sort_of env sigma t = let _,f,_,_ = retype sigma in f env t -let get_sort_family_of env sigma c = let _,_,f,_ = retype sigma in f env c +let get_sort_of ?(polyprop=true) env sigma t = + let _,f,_,_ = retype ~polyprop sigma in f env t +let get_sort_family_of ?(polyprop=true) env sigma c = + let _,_,f,_ = retype ~polyprop sigma in f env c let type_of_global_reference_knowing_parameters env sigma c args = let _,_,_,f = retype sigma in f env c args @@ -161,8 +163,8 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty = (* We are outside the kernel: we take fresh universes *) (* to avoid tactics and co to refresh universes themselves *) -let get_type_of ?(refresh=true) env sigma c = - let f,_,_,_ = retype sigma in +let get_type_of ?(polyprop=true) ?(refresh=true) env sigma c = + let f,_,_,_ = retype ~polyprop sigma in let t = f env c in if refresh then refresh_universes t else t diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index 98a3ff42..f2c030f9 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.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: retyping.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: retyping.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Names @@ -21,9 +21,17 @@ open Environ either produces a wrong result or raise an anomaly. Use with care. It doesn't handle predicative universes too. *) -val get_type_of : ?refresh:bool -> env -> evar_map -> constr -> types -val get_sort_of : env -> evar_map -> types -> sorts -val get_sort_family_of : env -> evar_map -> types -> sorts_family +(** The "polyprop" optional argument is used by the extraction to + disable "Prop-polymorphism", cf comment in [inductive.ml] *) + +val get_type_of : + ?polyprop:bool -> ?refresh:bool -> env -> evar_map -> constr -> types + +val get_sort_of : + ?polyprop:bool -> env -> evar_map -> types -> sorts + +val get_sort_family_of : + ?polyprop:bool -> env -> evar_map -> types -> sorts_family (* Makes an assumption from a constr *) val get_assumption_of : env -> evar_map -> constr -> types diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 68a67402..bd1eed94 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.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: tacred.ml 13804 2011-01-27 00:41:34Z letouzey $ *) +(* $Id: tacred.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Pp open Util diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index 064d2ce4..55c305cc 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.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: tacred.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: tacred.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Names diff --git a/pretyping/term_dnet.ml b/pretyping/term_dnet.ml index 0dfee738..9dda5143 100644 --- a/pretyping/term_dnet.ml +++ b/pretyping/term_dnet.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/pretyping/term_dnet.mli b/pretyping/term_dnet.mli index a8ac4119..9c4c9dbc 100644 --- a/pretyping/term_dnet.mli +++ b/pretyping/term_dnet.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/pretyping/termops.ml b/pretyping/termops.ml index a2759688..70f2279c 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.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: termops.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: termops.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Pp open Util diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 7977fe28..91c76564 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.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: termops.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: termops.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) open Util open Pp diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index d75032e7..9e64143d 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.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: typeclasses.ml 13332 2010-07-26 22:12:43Z msozeau $ i*) +(*i $Id: typeclasses.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Names @@ -299,9 +299,11 @@ let instance_constructor cl args = let lenpars = List.length (List.filter (fun (na, b, t) -> b = None) (snd cl.cl_context)) in let pars = fst (list_chop lenpars args) in match cl.cl_impl with - | IndRef ind -> applistc (mkConstruct (ind, 1)) args, + | IndRef ind -> Some (applistc (mkConstruct (ind, 1)) args), applistc (mkInd ind) pars - | ConstRef cst -> list_last args, applistc (mkConst cst) pars + | ConstRef cst -> + let term = if args = [] then None else Some (list_last args) in + term, applistc (mkConst cst) pars | _ -> assert false let typeclasses () = Gmap.fold (fun _ l c -> l :: c) !classes [] diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 8e1c2a92..83ae84a5 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.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: typeclasses.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: typeclasses.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Names @@ -75,7 +75,7 @@ val is_implicit_arg : hole_kind -> bool (* Returns the term and type for the given instance of the parameters and fields of the type class. *) -val instance_constructor : typeclass -> constr list -> constr * types +val instance_constructor : typeclass -> constr list -> constr option * types (* Use evar_extra for marking resolvable evars. *) val bool_in : bool -> Dyn.t diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index b3ab1f07..62941a76 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.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: typeclasses_errors.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: typeclasses_errors.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Names diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli index 94e1a57d..a763a80b 100644 --- a/pretyping/typeclasses_errors.mli +++ b/pretyping/typeclasses_errors.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: typeclasses_errors.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: typeclasses_errors.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Names diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 82b59d16..80db26a4 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.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: typing.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: typing.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Util open Names diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 32b64c5f..07cb7d59 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.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: typing.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: typing.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Term diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 02af6090..7aa2272d 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.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: unification.ml 13332 2010-07-26 22:12:43Z msozeau $ *) +(* $Id: unification.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Pp open Util diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 419d5d4f..2f48081a 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.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: unification.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: unification.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Term diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 2c8705d5..395f5c8d 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.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: vnorm.ml 13351 2010-07-29 15:26:31Z barras $ i*) +(*i $Id: vnorm.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) open Names open Declarations diff --git a/pretyping/vnorm.mli b/pretyping/vnorm.mli index ec8af8d4..4cf99842 100644 --- a/pretyping/vnorm.mli +++ b/pretyping/vnorm.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 *) |