diff options
Diffstat (limited to 'plugins/firstorder')
-rw-r--r-- | plugins/firstorder/formula.ml | 72 | ||||
-rw-r--r-- | plugins/firstorder/formula.mli | 25 | ||||
-rw-r--r-- | plugins/firstorder/g_ground.ml4 | 56 | ||||
-rw-r--r-- | plugins/firstorder/ground.ml | 16 | ||||
-rw-r--r-- | plugins/firstorder/ground.mli | 4 | ||||
-rw-r--r-- | plugins/firstorder/instances.ml | 82 | ||||
-rw-r--r-- | plugins/firstorder/instances.mli | 7 | ||||
-rw-r--r-- | plugins/firstorder/rules.ml | 102 | ||||
-rw-r--r-- | plugins/firstorder/rules.mli | 14 | ||||
-rw-r--r-- | plugins/firstorder/sequent.ml | 62 | ||||
-rw-r--r-- | plugins/firstorder/sequent.mli | 14 | ||||
-rw-r--r-- | plugins/firstorder/unify.ml | 28 | ||||
-rw-r--r-- | plugins/firstorder/unify.mli | 2 |
13 files changed, 240 insertions, 244 deletions
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index 79d4c5b5..62a8605a 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -9,13 +9,12 @@ open Hipattern open Names open Term +open Vars open Termops -open Reductionops open Tacmach open Util open Declarations -open Libnames -open Inductiveops +open Globnames let qflag=ref true @@ -23,11 +22,11 @@ let red_flags=ref Closure.betaiotazeta let (=?) f g i1 i2 j1 j2= let c=f i1 i2 in - if c=0 then g j1 j2 else c + if Int.equal c 0 then g j1 j2 else c let (==?) fg h i1 i2 j1 j2 k1 k2= let c=fg i1 i2 j1 j2 in - if c=0 then h k1 k2 else c + if Int.equal c 0 then h k1 k2 else c type ('a,'b) sum = Left of 'a | Right of 'b @@ -44,7 +43,7 @@ let rec nb_prod_after n c= | _ -> 0 let construct_nhyps ind gls = - let nparams = (fst (Global.lookup_inductive ind)).mind_nparams in + let nparams = (fst (Global.lookup_inductive (fst ind))).mind_nparams in let constr_types = Inductiveops.arities_of_constructors (pf_env gls) ind in let hyp = nb_prod_after nparams in Array.map hyp constr_types @@ -52,12 +51,11 @@ let construct_nhyps ind gls = (* indhyps builds the array of arrays of constructor hyps for (ind largs)*) let ind_hyps nevar ind largs gls= let types= Inductiveops.arities_of_constructors (pf_env gls) ind in - let lp=Array.length types in - let myhyps i= - let t1=Term.prod_applist types.(i) largs in + let myhyps t = + let t1=prod_applist t largs in let t2=snd (decompose_prod_n_assum nevar t1) in fst (decompose_prod_assum t2) in - Array.init lp myhyps + Array.map myhyps types let special_nf gl= let infos=Closure.create_clos_infos !red_flags (pf_env gl) in @@ -69,14 +67,14 @@ let special_whd gl= type kind_of_formula= Arrow of constr*constr - | False of inductive*constr list - | And of inductive*constr list*bool - | Or of inductive*constr list*bool - | Exists of inductive*constr list + | False of pinductive*constr list + | And of pinductive*constr list*bool + | Or of pinductive*constr list*bool + | Exists of pinductive*constr list | Forall of constr*constr | Atom of constr -let rec kind_of_formula gl term = +let kind_of_formula gl term = let normalize=special_nf gl in let cciterm=special_whd gl term in match match_with_imp_term cciterm with @@ -87,26 +85,26 @@ let rec kind_of_formula gl term = |_-> match match_with_nodep_ind cciterm with Some (i,l,n)-> - let ind=destInd i in + let ind,u=destInd i in let (mib,mip) = Global.lookup_inductive ind in let nconstr=Array.length mip.mind_consnames in - if nconstr=0 then - False(ind,l) + if Int.equal nconstr 0 then + False((ind,u),l) else let has_realargs=(n>0) in let is_trivial= let is_constant c = - nb_prod c = mib.mind_nparams in - array_exists is_constant mip.mind_nf_lc in + Int.equal (nb_prod c) mib.mind_nparams in + Array.exists is_constant mip.mind_nf_lc in if Inductiveops.mis_is_recursive (ind,mib,mip) || (has_realargs && not is_trivial) then Atom cciterm else - if nconstr=1 then - And(ind,l,is_trivial) + if Int.equal nconstr 1 then + And((ind,u),l,is_trivial) else - Or(ind,l,is_trivial) + Or((ind,u),l,is_trivial) | _ -> match match_with_sigma_type cciterm with Some (i,l)-> Exists((destInd i),l) @@ -118,7 +116,7 @@ type side = Hyp | Concl | Hint let no_atoms = (false,{positive=[];negative=[]}) -let dummy_id=VarRef (id_of_string "_") (* "_" cannot be parsed *) +let dummy_id=VarRef (Id.of_string "_") (* "_" cannot be parsed *) let build_atoms gl metagen side cciterm = let trivial =ref false @@ -144,9 +142,9 @@ let build_atoms gl metagen side cciterm = let g i _ (_,_,t) = build_rec env polarity (lift i t) in let f l = - list_fold_left_i g (1-(List.length l)) () l in + List.fold_left_i g (1-(List.length l)) () l in if polarity && (* we have a constant constructor *) - array_exists (function []->true|_->false) v + Array.exists (function []->true|_->false) v then trivial:=true; Array.iter f v | Exists(i,l)-> @@ -154,7 +152,7 @@ let build_atoms gl metagen side cciterm = let v =(ind_hyps 1 i l gl).(0) in let g i _ (_,_,t) = build_rec (var::env) polarity (lift i t) in - list_fold_left_i g (2-(List.length l)) () v + List.fold_left_i g (2-(List.length l)) () v | Forall(_,b)-> let var=mkMeta (metagen true) in build_rec (var::env) polarity b @@ -171,7 +169,7 @@ let build_atoms gl metagen side cciterm = | Hyp -> build_rec [] false cciterm | Hint -> let rels,head=decompose_prod cciterm in - let env=List.rev (List.map (fun _->mkMeta (metagen true)) rels) in + let env=List.rev_map (fun _->mkMeta (metagen true)) rels in build_rec env false head;trivial:=false (* special for hints *) end; (!trivial, @@ -188,19 +186,19 @@ type right_pattern = type left_arrow_pattern= LLatom - | LLfalse of inductive*constr list - | LLand of inductive*constr list - | LLor of inductive*constr list + | LLfalse of pinductive*constr list + | LLand of pinductive*constr list + | LLor of pinductive*constr list | LLforall of constr - | LLexists of inductive*constr list + | LLexists of pinductive*constr list | LLarrow of constr*constr*constr type left_pattern= Lfalse - | Land of inductive - | Lor of inductive + | Land of pinductive + | Lor of pinductive | Lforall of metavariable*constr*bool - | Lexists of inductive + | Lexists of pinductive | LA of constr*left_arrow_pattern type t={id:global_reference; @@ -226,7 +224,7 @@ let build_formula side nam typ gl metagen= | And(_,_,_) -> Rand | Or(_,_,_) -> Ror | Exists (i,l) -> - let (_,_,d)=list_last (ind_hyps 0 i l gl).(0) in + let (_,_,d)=List.last (ind_hyps 0 i l gl).(0) in Rexists(m,d,trivial) | Forall (_,a) -> Rforall | Arrow (a,b) -> Rarrow in diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli index 44bbb335..29ea1e77 100644 --- a/plugins/firstorder/formula.mli +++ b/plugins/firstorder/formula.mli @@ -1,14 +1,15 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term open Names -open Libnames +open Term +open Context +open Globnames val qflag : bool ref @@ -24,9 +25,9 @@ type ('a,'b) sum = Left of 'a | Right of 'b type counter = bool -> metavariable -val construct_nhyps : inductive -> Proof_type.goal Tacmach.sigma -> int array +val construct_nhyps : pinductive -> Proof_type.goal Tacmach.sigma -> int array -val ind_hyps : int -> inductive -> constr list -> +val ind_hyps : int -> pinductive -> constr list -> Proof_type.goal Tacmach.sigma -> rel_context array type atoms = {positive:constr list;negative:constr list} @@ -48,19 +49,19 @@ type right_pattern = type left_arrow_pattern= LLatom - | LLfalse of inductive*constr list - | LLand of inductive*constr list - | LLor of inductive*constr list + | LLfalse of pinductive*constr list + | LLand of pinductive*constr list + | LLor of pinductive*constr list | LLforall of constr - | LLexists of inductive*constr list + | LLexists of pinductive*constr list | LLarrow of constr*constr*constr type left_pattern= Lfalse - | Land of inductive - | Lor of inductive + | Land of pinductive + | Lor of pinductive | Lforall of metavariable*constr*bool - | Lexists of inductive + | Lexists of pinductive | LA of constr*left_arrow_pattern type t={id: global_reference; diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 5b882036..c28da42a 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -1,25 +1,23 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Formula open Sequent open Ground open Goptions -open Tactics open Tacticals open Tacinterp -open Term -open Names -open Util open Libnames +DECLARE PLUGIN "ground_plugin" + (* declaring search depth as a global option *) let ground_depth=ref 3 @@ -57,16 +55,16 @@ let _= let (set_default_solver, default_solver, print_default_solver) = Tactic_option.declare_tactic_option ~default:(<:tactic<auto with *>>) "Firstorder default solver" -VERNAC COMMAND EXTEND Firstorder_Set_Solver +VERNAC COMMAND EXTEND Firstorder_Set_Solver CLASSIFIED AS SIDEFF | [ "Set" "Firstorder" "Solver" tactic(t) ] -> [ set_default_solver - (Vernacexpr.use_section_locality ()) - (Tacinterp.glob_tactic t) ] + (Locality.make_section_locality (Locality.LocalityFixme.consume ())) + (Tacintern.glob_tactic t) ] END -VERNAC COMMAND EXTEND Firstorder_Print_Solver +VERNAC COMMAND EXTEND Firstorder_Print_Solver CLASSIFIED AS QUERY | [ "Print" "Firstorder" "Solver" ] -> [ - Pp.msgnl + Pp.msg_info (Pp.(++) (Pp.str"Firstorder solver tactic is ") (print_default_solver ())) ] END @@ -82,10 +80,11 @@ let gen_ground_tac flag taco ids bases gl= | None-> snd (default_solver ()) in let startseq gl= let seq=empty_seq !ground_depth in - extend_with_auto_hints bases (extend_with_ref_list ids seq gl) gl in - let result=ground_tac solver startseq gl in + let seq,gl = extend_with_ref_list ids seq gl in + extend_with_auto_hints bases seq gl in + let result=ground_tac (Proofview.V82.of_tactic solver) startseq gl in qflag:=backup;result - with reraise ->qflag:=backup;raise reraise + with reraise -> qflag:=backup;raise reraise (* special for compatibility with Intuition @@ -103,12 +102,13 @@ let normalize_evaluables= unfold_in_hyp (Lazy.force defined_connectives) (Tacexpr.InHypType id)) *) +open Pp open Genarg open Ppconstr open Printer -let pr_firstorder_using_raw _ _ _ = prlist_with_sep pr_comma pr_reference -let pr_firstorder_using_glob _ _ _ = prlist_with_sep pr_comma (pr_or_var (pr_located pr_global)) -let pr_firstorder_using_typed _ _ _ = prlist_with_sep pr_comma pr_global +let pr_firstorder_using_raw _ _ _ l = str "using " ++ prlist_with_sep pr_comma pr_reference l +let pr_firstorder_using_glob _ _ _ l = str "using " ++ prlist_with_sep pr_comma (pr_or_var (fun x -> (pr_global (snd x)))) l +let pr_firstorder_using_typed _ _ _ l = str "using " ++ prlist_with_sep pr_comma pr_global l ARGUMENT EXTEND firstorder_using PRINTED BY pr_firstorder_using_typed @@ -128,29 +128,31 @@ END TACTIC EXTEND firstorder [ "firstorder" tactic_opt(t) firstorder_using(l) ] -> - [ gen_ground_tac true (Option.map eval_tactic t) l [] ] + [ Proofview.V82.tactic (gen_ground_tac true (Option.map eval_tactic t) l []) ] | [ "firstorder" tactic_opt(t) "with" ne_preident_list(l) ] -> - [ gen_ground_tac true (Option.map eval_tactic t) [] l ] + [ Proofview.V82.tactic (gen_ground_tac true (Option.map eval_tactic t) [] l) ] | [ "firstorder" tactic_opt(t) firstorder_using(l) "with" ne_preident_list(l') ] -> - [ gen_ground_tac true (Option.map eval_tactic t) l l' ] + [ Proofview.V82.tactic (gen_ground_tac true (Option.map eval_tactic t) l l') ] END TACTIC EXTEND gintuition [ "gintuition" tactic_opt(t) ] -> - [ gen_ground_tac false (Option.map eval_tactic t) [] [] ] + [ Proofview.V82.tactic (gen_ground_tac false (Option.map eval_tactic t) [] []) ] END +open Proofview.Notations -let default_declarative_automation gls = - tclORELSE - (tclORELSE (Auto.h_trivial [] None) +let default_declarative_automation = + Proofview.tclUNIT () >>= fun () -> (* delay for [congruence_depth] *) + Tacticals.New.tclORELSE + (Tacticals.New.tclORELSE (Auto.h_trivial [] None) (Cctac.congruence_tac !congruence_depth [])) - (gen_ground_tac true - (Some (tclTHEN + (Proofview.V82.tactic (gen_ground_tac true + (Some (Tacticals.New.tclTHEN (snd (default_solver ())) (Cctac.congruence_tac !congruence_depth []))) - [] []) gls + [] [])) diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml index 7c80b9bb..2248b669 100644 --- a/plugins/firstorder/ground.ml +++ b/plugins/firstorder/ground.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -12,28 +12,27 @@ open Rules open Instances open Term open Tacmach -open Tactics open Tacticals -open Libnames let update_flags ()= let predref=ref Names.Cpred.empty in let f coe= try - let kn=destConst (Classops.get_coercion_value coe) in + let kn= fst (destConst (Classops.get_coercion_value coe)) in predref:=Names.Cpred.add kn !predref - with Invalid_argument "destConst"-> () in + with DestKO -> () + in List.iter f (Classops.coercions ()); red_flags:= Closure.RedFlags.red_add_transparent Closure.betaiotazeta - (Names.Idpred.full,Names.Cpred.complement !predref) + (Names.Id.Pred.full,Names.Cpred.complement !predref) let ground_tac solver startseq gl= update_flags (); let rec toptac skipped seq gl= if Tacinterp.get_debug()=Tactic_debug.DebugOn 0 - then Pp.msgnl (Printer.pr_goal gl); + then Pp.msg_debug (Printer.pr_goal gl); tclORELSE (axiom_tac seq.gl seq) begin try @@ -120,5 +119,6 @@ let ground_tac solver startseq gl= end with Heap.EmptyHeap->solver end gl in - wrap (List.length (pf_hyps gl)) true (toptac []) (startseq gl) gl + let seq, gl' = startseq gl in + wrap (List.length (pf_hyps gl)) true (toptac []) seq gl' diff --git a/plugins/firstorder/ground.mli b/plugins/firstorder/ground.mli index 380326e7..5b320786 100644 --- a/plugins/firstorder/ground.mli +++ b/plugins/firstorder/ground.mli @@ -1,11 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) val ground_tac: Tacmach.tactic -> - (Proof_type.goal Tacmach.sigma -> Sequent.t) -> Tacmach.tactic + (Proof_type.goal Tacmach.sigma -> Sequent.t * Proof_type.goal Tacmach.sigma) -> Tacmach.tactic diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index d45ab0c3..a88778c7 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -1,28 +1,27 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Formula -open Sequent open Unify open Rules +open Errors open Util open Term +open Vars open Glob_term open Tacmach open Tactics open Tacticals open Termops open Reductionops -open Declarations open Formula open Sequent open Names -open Libnames +open Misctypes let compare_instance inst1 inst2= match inst1,inst2 with @@ -30,18 +29,18 @@ let compare_instance inst1 inst2= (OrderedConstr.compare d1 d2) | Real((m1,c1),n1),Real((m2,c2),n2)-> ((-) =? (-) ==? OrderedConstr.compare) m2 m1 n1 n2 c1 c2 - | Phantom(_),Real((m,_),_)-> if m=0 then -1 else 1 - | Real((m,_),_),Phantom(_)-> if m=0 then 1 else -1 + | Phantom(_),Real((m,_),_)-> if Int.equal m 0 then -1 else 1 + | Real((m,_),_),Phantom(_)-> if Int.equal m 0 then 1 else -1 let compare_gr id1 id2 = if id1==id2 then 0 else if id1==dummy_id then 1 else if id2==dummy_id then -1 - else Libnames.RefOrdered.compare id1 id2 + else Globnames.RefOrdered.compare id1 id2 module OrderedInstance= struct - type t=instance * Libnames.global_reference + type t=instance * Globnames.global_reference let compare (inst1,id1) (inst2,id2)= (compare_instance =? compare_gr) inst2 inst1 id2 id1 (* we want a __decreasing__ total order *) @@ -76,7 +75,7 @@ let match_one_quantified_hyp setref seq lf= Left(Lforall(i,dom,triv))|Right(Rexists(i,dom,triv))-> if do_sequent setref triv lf.id seq i dom lf.atoms then setref:=IS.add ((Phantom dom),lf.id) !setref - | _ ->anomaly "can't happen" + | _ -> anomaly (Pp.str "can't happen") let give_instances lf seq= let setref=ref IS.empty in @@ -99,36 +98,36 @@ let rec collect_quantified seq= let dummy_constr=mkMeta (-1) -let dummy_bvid=id_of_string "x" +let dummy_bvid=Id.of_string "x" -let mk_open_instance id gl m t= +let mk_open_instance id idc gl m t= let env=pf_env gl in let evmap=Refiner.project gl in let var_id= if id==dummy_id then dummy_bvid else - let typ=pf_type_of gl (constr_of_global id) in + let typ=pf_type_of gl idc in (* since we know we will get a product, reduction is not too expensive *) let (nam,_,_)=destProd (whd_betadeltaiota env evmap typ) in match nam with Name id -> id | Anonymous -> dummy_bvid in - let revt=substl (list_tabulate (fun i->mkRel (m-i)) m) t in + let revt=substl (List.init m (fun i->mkRel (m-i))) t in let rec aux n avoid= - if n=0 then [] else + if Int.equal n 0 then [] else let nid=(fresh_id avoid var_id gl) in (Name nid,None,dummy_constr)::(aux (n-1) (nid::avoid)) in let nt=it_mkLambda_or_LetIn revt (aux m []) in - let rawt=Detyping.detype false [] [] nt in + let rawt=Detyping.detype false [] env evmap nt in let rec raux n t= - if n=0 then t else + if Int.equal n 0 then t else match t with GLambda(loc,name,k,_,t0)-> let t1=raux (n-1) t0 in - GLambda(loc,name,k,GHole (dummy_loc,Evd.BinderType name),t1) - | _-> anomaly "can't happen" in + GLambda(loc,name,k,GHole (Loc.ghost,Evar_kinds.BinderType name,Misctypes.IntroAnonymous,None),t1) + | _-> anomaly (Pp.str "can't happen") in let ntt=try - Pretyping.Default.understand evmap env (raux m rawt) + fst (Pretyping.understand env evmap (raux m rawt))(*FIXME*) with e when Errors.noncritical e -> error "Untypable instance, maybe higher-order non-prenex quantification" in decompose_lam_n_assum m ntt @@ -141,50 +140,53 @@ let left_instance_tac (inst,id) continue seq= if lookup (id,None) seq then tclFAIL 0 (Pp.str "already done") else - tclTHENS (cut dom) + tclTHENS (Proofview.V82.of_tactic (cut dom)) [tclTHENLIST - [introf; + [Proofview.V82.of_tactic introf; + pf_constr_of_global id (fun idc -> (fun gls->generalize - [mkApp(constr_of_global id, - [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls); - introf; + [mkApp(idc, + [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls)); + Proofview.V82.of_tactic introf; tclSOLVE [wrap 1 false continue (deepen (record (id,None) seq))]]; - tclTRY assumption] + tclTRY (Proofview.V82.of_tactic assumption)] | Real((m,t) as c,_)-> if lookup (id,Some c) seq then tclFAIL 0 (Pp.str "already done") else let special_generalize= if m>0 then - fun gl-> - let (rc,ot)= mk_open_instance id gl m t in - let gt= - it_mkLambda_or_LetIn - (mkApp(constr_of_global id,[|ot|])) rc in - generalize [gt] gl + pf_constr_of_global id (fun idc -> + fun gl-> + let (rc,ot) = mk_open_instance id idc gl m t in + let gt= + it_mkLambda_or_LetIn + (mkApp(idc,[|ot|])) rc in + generalize [gt] gl) else - generalize [mkApp(constr_of_global id,[|t|])] + pf_constr_of_global id (fun idc -> + generalize [mkApp(idc,[|t|])]) in tclTHENLIST [special_generalize; - introf; + Proofview.V82.of_tactic introf; tclSOLVE [wrap 1 false continue (deepen (record (id,Some c) seq))]] let right_instance_tac inst continue seq= match inst with Phantom dom -> - tclTHENS (cut dom) + tclTHENS (Proofview.V82.of_tactic (cut dom)) [tclTHENLIST - [introf; + [Proofview.V82.of_tactic introf; (fun gls-> - split (Glob_term.ImplicitBindings - [mkVar (Tacmach.pf_nth_hyp_id gls 1)]) gls); + Proofview.V82.of_tactic (split (ImplicitBindings + [mkVar (Tacmach.pf_nth_hyp_id gls 1)])) gls); tclSOLVE [wrap 0 true continue (deepen seq)]]; - tclTRY assumption] + tclTRY (Proofview.V82.of_tactic assumption)] | Real ((0,t),_) -> - (tclTHEN (split (Glob_term.ImplicitBindings [t])) + (tclTHEN (Proofview.V82.of_tactic (split (ImplicitBindings [t]))) (tclSOLVE [wrap 0 true continue (deepen seq)])) | Real ((m,t),_) -> tclFAIL 0 (Pp.str "not implemented ... yet") diff --git a/plugins/firstorder/instances.mli b/plugins/firstorder/instances.mli index 709eb96f..2f69ad7b 100644 --- a/plugins/firstorder/instances.mli +++ b/plugins/firstorder/instances.mli @@ -1,15 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term -open Tacmach -open Names -open Libnames +open Globnames open Rules val collect_quantified : Sequent.t -> Formula.t list * Sequent.t diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index b043ba5f..382d5409 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -1,22 +1,24 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Names open Term +open Vars open Tacmach open Tactics open Tacticals open Termops -open Declarations open Formula open Sequent -open Libnames +open Globnames +open Locus type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic @@ -25,13 +27,13 @@ type lseqtac= global_reference -> seqtac type 'a with_backtracking = tactic -> 'a let wrap n b continue seq gls= - check_for_interrupt (); + Control.check_for_interrupt (); let nc=pf_hyps gls in let env=pf_env gls in let rec aux i nc ctx= if i<=0 then seq else match nc with - []->anomaly "Not the expected number of hyps" + []->anomaly (Pp.str "Not the expected number of hyps") | ((id,_,typ) as nd)::q-> if occur_var env id (pf_concl gls) || List.exists (occur_var_in_decl env id) ctx then @@ -51,38 +53,38 @@ let clear_global=function VarRef id->clear [id] | _->tclIDTAC - (* connection rules *) let axiom_tac t seq= - try exact_no_check (constr_of_global (find_left t seq)) + try pf_constr_of_global (find_left t seq) exact_no_check with Not_found->tclFAIL 0 (Pp.str "No axiom link") let ll_atom_tac a backtrack id continue seq= tclIFTHENELSE (try tclTHENLIST - [generalize [mkApp(constr_of_global id, - [|constr_of_global (find_left a seq)|])]; + [pf_constr_of_global (find_left a seq) (fun left -> + pf_constr_of_global id (fun id -> + generalize [mkApp(id, [|left|])])); clear_global id; - intro] + Proofview.V82.of_tactic intro] with Not_found->tclFAIL 0 (Pp.str "No link")) (wrap 1 false continue seq) backtrack (* right connectives rules *) let and_tac backtrack continue seq= - tclIFTHENELSE simplest_split (wrap 0 true continue seq) backtrack + tclIFTHENELSE (Proofview.V82.of_tactic simplest_split) (wrap 0 true continue seq) backtrack let or_tac backtrack continue seq= tclORELSE - (any_constructor false (Some (tclCOMPLETE (wrap 0 true continue seq)))) + (Proofview.V82.of_tactic (any_constructor false (Some (Proofview.V82.tactic (tclCOMPLETE (wrap 0 true continue seq)))))) backtrack let arrow_tac backtrack continue seq= - tclIFTHENELSE intro (wrap 1 true continue seq) + tclIFTHENELSE (Proofview.V82.of_tactic intro) (wrap 1 true continue seq) (tclORELSE - (tclTHEN introf (tclCOMPLETE (wrap 1 true continue seq))) + (tclTHEN (Proofview.V82.of_tactic introf) (tclCOMPLETE (wrap 1 true continue seq))) backtrack) (* left connectives rules *) @@ -90,9 +92,9 @@ let left_and_tac ind backtrack id continue seq gls= let n=(construct_nhyps ind gls).(0) in tclIFTHENELSE (tclTHENLIST - [simplest_elim (constr_of_global id); + [Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim); clear_global id; - tclDO n intro]) + tclDO n (Proofview.V82.of_tactic intro)]) (wrap n false continue seq) backtrack gls @@ -101,59 +103,58 @@ let left_or_tac ind backtrack id continue seq gls= let f n= tclTHENLIST [clear_global id; - tclDO n intro; + tclDO n (Proofview.V82.of_tactic intro); wrap n false continue seq] in tclIFTHENSVELSE - (simplest_elim (constr_of_global id)) + (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim)) (Array.map f v) backtrack gls let left_false_tac id= - simplest_elim (constr_of_global id) + Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim) (* left arrow connective rules *) (* We use this function for false, and, or, exists *) -let ll_ind_tac ind largs backtrack id continue seq gl= - let rcs=ind_hyps 0 ind largs gl in +let ll_ind_tac (ind,u as indu) largs backtrack id continue seq gl= + let rcs=ind_hyps 0 indu largs gl in let vargs=Array.of_list largs in - (* construire le terme H->B, le generaliser etc *) - let myterm i= + (* construire le terme H->B, le generaliser etc *) + let myterm idc i= let rc=rcs.(i) in let p=List.length rc in - let cstr=mkApp ((mkConstruct (ind,(i+1))),vargs) in + let cstr=mkApp ((mkConstructU ((ind,(i+1)),u)),vargs) in let vars=Array.init p (fun j->mkRel (p-j)) in let capply=mkApp ((lift p cstr),vars) in - let head=mkApp ((lift p (constr_of_global id)),[|capply|]) in - it_mkLambda_or_LetIn head rc in + let head=mkApp ((lift p idc),[|capply|]) in + it_mkLambda_or_LetIn head rc in let lp=Array.length rcs in - let newhyps=list_tabulate myterm lp in + let newhyps idc =List.init lp (myterm idc) in tclIFTHENELSE (tclTHENLIST - [generalize newhyps; + [pf_constr_of_global id (fun idc -> generalize (newhyps idc)); clear_global id; - tclDO lp intro]) + tclDO lp (Proofview.V82.of_tactic intro)]) (wrap lp false continue seq) backtrack gl let ll_arrow_tac a b c backtrack id continue seq= let cc=mkProd(Anonymous,a,(lift 1 b)) in - let d=mkLambda (Anonymous,b, - mkApp ((constr_of_global id), - [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in + let d idc =mkLambda (Anonymous,b, + mkApp (idc, [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in tclORELSE - (tclTHENS (cut c) + (tclTHENS (Proofview.V82.of_tactic (cut c)) [tclTHENLIST - [introf; + [Proofview.V82.of_tactic introf; clear_global id; wrap 1 false continue seq]; - tclTHENS (cut cc) - [exact_no_check (constr_of_global id); + tclTHENS (Proofview.V82.of_tactic (cut cc)) + [pf_constr_of_global id exact_no_check; tclTHENLIST - [generalize [d]; + [pf_constr_of_global id (fun idc -> generalize [d idc]); clear_global id; - introf; - introf; + Proofview.V82.of_tactic introf; + Proofview.V82.of_tactic introf; tclCOMPLETE (wrap 2 true continue seq)]]]) backtrack @@ -161,9 +162,9 @@ let ll_arrow_tac a b c backtrack id continue seq= let forall_tac backtrack continue seq= tclORELSE - (tclIFTHENELSE intro (wrap 0 true continue seq) + (tclIFTHENELSE (Proofview.V82.of_tactic intro) (wrap 0 true continue seq) (tclORELSE - (tclTHEN introf (tclCOMPLETE (wrap 0 true continue seq))) + (tclTHEN (Proofview.V82.of_tactic introf) (tclCOMPLETE (wrap 0 true continue seq))) backtrack)) (if !qflag then tclFAIL 0 (Pp.str "reversible in 1st order mode") @@ -173,24 +174,25 @@ let forall_tac backtrack continue seq= let left_exists_tac ind backtrack id continue seq gls= let n=(construct_nhyps ind gls).(0) in tclIFTHENELSE - (simplest_elim (constr_of_global id)) + (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim)) (tclTHENLIST [clear_global id; - tclDO n intro; + tclDO n (Proofview.V82.of_tactic intro); (wrap (n-1) false continue seq)]) backtrack gls let ll_forall_tac prod backtrack id continue seq= tclORELSE - (tclTHENS (cut prod) + (tclTHENS (Proofview.V82.of_tactic (cut prod)) [tclTHENLIST - [intro; + [Proofview.V82.of_tactic intro; + pf_constr_of_global id (fun idc -> (fun gls-> let id0=pf_nth_hyp_id gls 1 in - let term=mkApp((constr_of_global id),[|mkVar(id0)|]) in - tclTHEN (generalize [term]) (clear [id0]) gls); + let term=mkApp(idc,[|mkVar(id0)|]) in + tclTHEN (generalize [term]) (clear [id0]) gls)); clear_global id; - intro; + Proofview.V82.of_tactic intro; tclCOMPLETE (wrap 1 false continue (deepen seq))]; tclCOMPLETE (wrap 0 true continue (deepen seq))]) backtrack @@ -202,8 +204,8 @@ let ll_forall_tac prod backtrack id continue seq= let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str let defined_connectives=lazy - [all_occurrences,EvalConstRef (destConst (constant "not")); - all_occurrences,EvalConstRef (destConst (constant "iff"))] + [AllOccurrences,EvalConstRef (fst (destConst (constant "not"))); + AllOccurrences,EvalConstRef (fst (destConst (constant "iff")))] let normalize_evaluables= onAllHypsAndConcl diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli index d5fe398f..596e8535 100644 --- a/plugins/firstorder/rules.mli +++ b/plugins/firstorder/rules.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -9,7 +9,7 @@ open Term open Tacmach open Names -open Libnames +open Globnames type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic @@ -19,7 +19,7 @@ type 'a with_backtracking = tactic -> 'a val wrap : int -> bool -> seqtac -val basename_of_global: global_reference -> identifier +val basename_of_global: global_reference -> Id.t val clear_global: global_reference -> tactic @@ -33,19 +33,19 @@ val or_tac : seqtac with_backtracking val arrow_tac : seqtac with_backtracking -val left_and_tac : inductive -> lseqtac with_backtracking +val left_and_tac : pinductive -> lseqtac with_backtracking -val left_or_tac : inductive -> lseqtac with_backtracking +val left_or_tac : pinductive -> lseqtac with_backtracking val left_false_tac : global_reference -> tactic -val ll_ind_tac : inductive -> constr list -> lseqtac with_backtracking +val ll_ind_tac : pinductive -> constr list -> lseqtac with_backtracking val ll_arrow_tac : constr -> constr -> constr -> lseqtac with_backtracking val forall_tac : seqtac with_backtracking -val left_exists_tac : inductive -> lseqtac with_backtracking +val left_exists_tac : pinductive -> lseqtac with_backtracking val ll_forall_tac : types -> lseqtac with_backtracking diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 50cf14a9..2f7f21e4 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -1,18 +1,18 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) open Term +open Errors open Util open Formula open Unify open Tacmach -open Names -open Libnames +open Globnames open Pp let newcnt ()= @@ -48,8 +48,6 @@ let priority = (* pure heuristics, <=0 for non reversible *) | LLexists (_,_) -> 50 | LLarrow (_,_,_) -> -10 -let left_reversible lpat=(priority lpat)>0 - module OrderedFormula= struct type t=Formula.t @@ -69,12 +67,14 @@ module Hitem= struct type t = h_item let compare (id1,co1) (id2,co2)= - (Libnames.RefOrdered.compare - =? (fun oc1 oc2 -> - match oc1,oc2 with - Some (m1,c1),Some (m2,c2) -> - ((-) =? OrderedConstr.compare) m1 m2 c1 c2 - | _,_->Pervasives.compare oc1 oc2)) id1 id2 co1 co2 + let c = Globnames.RefOrdered.compare id1 id2 in + if c = 0 then + let cmp (i1, c1) (i2, c2) = + let c = Int.compare i1 i2 in + if c = 0 then OrderedConstr.compare c1 c2 else c + in + Option.compare cmp co1 co2 + else c end module CM=Map.Make(OrderedConstr) @@ -90,7 +90,7 @@ let cm_add typ nam cm= let cm_remove typ nam cm= try let l=CM.find typ cm in - let l0=List.filter (fun id->id<>nam) l in + let l0=List.filter (fun id-> not (Globnames.eq_gr id nam)) l in match l0 with []->CM.remove typ cm | _ ->CM.add typ l0 cm @@ -120,10 +120,10 @@ let lookup item seq= let p (id2,o)= match o with None -> false - | Some ((m2,t2) as c2)->id=id2 && m2>m && more_general c2 c in + | Some ((m2,t2) as c2)-> Globnames.eq_gr id id2 && m2>m && more_general c2 c in History.exists p seq.history -let rec add_formula side nam t seq gl= +let add_formula side nam t seq gl= match build_formula side nam t gl seq.cnt with Left f-> begin @@ -163,8 +163,6 @@ let find_left t seq=List.hd (CM.find t seq.context) left_reversible lpat with Heap.EmptyHeap -> false *) -let no_formula seq= - seq.redexes=HP.empty let rec take_formula seq= let hd=HP.maximum seq.redexes @@ -191,36 +189,36 @@ let empty_seq depth= depth=depth} let expand_constructor_hints = - list_map_append (function + List.map_append (function | IndRef ind -> - list_tabulate (fun i -> ConstructRef (ind,i+1)) - (Inductiveops.nconstructors ind) + List.init (Inductiveops.nconstructors ind) + (fun i -> ConstructRef (ind,i+1)) | gr -> [gr]) -let extend_with_ref_list l seq gl= +let extend_with_ref_list l seq gl = let l = expand_constructor_hints l in - let f gr seq= - let c=constr_of_global gr in + let f gr (seq,gl) = + let gl, c = pf_eapply Evd.fresh_global gl gr in let typ=(pf_type_of gl c) in - add_formula Hyp gr typ seq gl in - List.fold_right f l seq + (add_formula Hyp gr typ seq gl,gl) in + List.fold_right f l (seq,gl) -open Auto +open Hints let extend_with_auto_hints l seq gl= let seqref=ref seq in let f p_a_t = match p_a_t.code with - Res_pf (c,_) | Give_exact c + Res_pf (c,_) | Give_exact (c,_) | Res_pf_THEN_trivial_fail (c,_) -> (try - let gr=global_of_constr c in + let gr = global_of_constr c in let typ=(pf_type_of gl c) in seqref:=add_formula Hint gr typ !seqref gl with Not_found->()) | _-> () in - let g _ l = List.iter f l in + let g _ _ l = List.iter f l in let h dbname= let hdb= try @@ -229,18 +227,18 @@ let extend_with_auto_hints l seq gl= error ("Firstorder: "^dbname^" : No such Hint database") in Hint_db.iter g hdb in List.iter h l; - !seqref + !seqref, gl (*FIXME: forgetting about universes*) let print_cmap map= let print_entry c l s= - let xc=Constrextern.extern_constr false (Global.env ()) c in + let xc=Constrextern.extern_constr false (Global.env ()) Evd.empty c in str "| " ++ - Util.prlist Printer.pr_global l ++ + prlist Printer.pr_global l ++ str " : " ++ Ppconstr.pr_constr_expr xc ++ cut () ++ s in - msgnl (v 0 + (v 0 (str "-----" ++ cut () ++ CM.fold print_entry map (mt ()) ++ diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli index 44b5ed3e..dc3f05be 100644 --- a/plugins/firstorder/sequent.mli +++ b/plugins/firstorder/sequent.mli @@ -1,17 +1,15 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) open Term -open Util open Formula open Tacmach -open Names -open Libnames +open Globnames module OrderedConstr: Set.OrderedType with type t=constr @@ -56,9 +54,9 @@ val take_formula : t -> Formula.t * t val empty_seq : int -> t val extend_with_ref_list : global_reference list -> - t -> Proof_type.goal sigma -> t + t -> Proof_type.goal sigma -> t * Proof_type.goal sigma -val extend_with_auto_hints : Auto.hint_db_name list -> - t -> Proof_type.goal sigma -> t +val extend_with_auto_hints : Hints.hint_db_name list -> + t -> Proof_type.goal sigma -> t * Proof_type.goal sigma -val print_cmap: global_reference list CM.t -> unit +val print_cmap: global_reference list CM.t -> Pp.std_ppcmds diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index 00eb9981..0a172034 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -1,16 +1,14 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) open Util -open Formula -open Tacmach open Term -open Names +open Vars open Termops open Reductionops @@ -34,7 +32,7 @@ let unif t1 t2= match kind_of_term t with Meta i-> (try - head_reduce (List.assoc i !sigma) + head_reduce (Int.List.assoc i !sigma) with Not_found->t) | _->t in Queue.add (t1,t2) bige; @@ -44,17 +42,17 @@ let unif t1 t2= and nt2=head_reduce (whd_betaiotazeta Evd.empty t2) in match (kind_of_term nt1),(kind_of_term nt2) with Meta i,Meta j-> - if i<>j then + if not (Int.equal i j) then if i<j then bind j nt1 else bind i nt2 | Meta i,_ -> let t=subst_meta !sigma nt2 in - if Intset.is_empty (free_rels t) && + if Int.Set.is_empty (free_rels t) && not (occur_term (mkMeta i) t) then bind i t else raise (UFAIL(nt1,nt2)) | _,Meta i -> let t=subst_meta !sigma nt1 in - if Intset.is_empty (free_rels t) && + if Int.Set.is_empty (free_rels t) && not (occur_term (mkMeta i) t) then bind i t else raise (UFAIL(nt1,nt2)) | Cast(_,_,_),_->Queue.add (strip_outer_cast nt1,nt2) bige @@ -65,7 +63,7 @@ let unif t1 t2= Queue.add (pa,pb) bige; Queue.add (ca,cb) bige; let l=Array.length va in - if l<>(Array.length vb) then + if not (Int.equal l (Array.length vb)) then raise (UFAIL (nt1,nt2)) else for i=0 to l-1 do @@ -74,13 +72,13 @@ let unif t1 t2= | App(ha,va),App(hb,vb)-> Queue.add (ha,hb) bige; let l=Array.length va in - if l<>(Array.length vb) then + if not (Int.equal l (Array.length vb)) then raise (UFAIL (nt1,nt2)) else for i=0 to l-1 do Queue.add (va.(i),vb.(i)) bige done - | _->if not (eq_constr nt1 nt2) then raise (UFAIL (nt1,nt2)) + | _->if not (eq_constr_nounivs nt1 nt2) then raise (UFAIL (nt1,nt2)) done; assert false (* this place is unreachable but needed for the sake of typing *) @@ -90,7 +88,7 @@ let value i t= let add x y= if x<0 then y else if y<0 then x else x+y in let rec vaux term= - if isMeta term && destMeta term = i then 0 else + if isMeta term && Int.equal (destMeta term) i then 0 else let f v t=add v (vaux t) in let vr=fold_constr f (-1) term in if vr<0 then -1 else vr+1 in @@ -107,7 +105,7 @@ let mk_rel_inst t= match kind_of_term t with Meta n-> (try - mkRel (d+(List.assoc n !rel_env)) + mkRel (d+(Int.List.assoc n !rel_env)) with Not_found-> let m= !new_rel in incr new_rel; @@ -119,7 +117,7 @@ let mk_rel_inst t= let unif_atoms i dom t1 t2= try - let t=List.assoc i (unif t1 t2) in + let t=Int.List.assoc i (unif t1 t2) in if isMeta t then Some (Phantom dom) else Some (Real(mk_rel_inst t,value i t1)) with @@ -127,7 +125,7 @@ let unif_atoms i dom t1 t2= | Not_found ->Some (Phantom dom) let renum_metas_from k n t= (* requires n = max (free_rels t) *) - let l=list_tabulate (fun i->mkMeta (k+i)) n in + let l=List.init n (fun i->mkMeta (k+i)) in substl l t let more_general (m1,t1) (m2,t2)= diff --git a/plugins/firstorder/unify.mli b/plugins/firstorder/unify.mli index 697548be..15318546 100644 --- a/plugins/firstorder/unify.mli +++ b/plugins/firstorder/unify.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) |