From 82183b138d009e90a2d3381eb84bab6f46dbc728 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 12 Jul 2006 12:20:18 +0000 Subject: [PATCH] Missing copyright added to tactics/declarative.ml* --- .../components/tactics/declarative.ml | 26 ++++++++++++++++++- .../components/tactics/declarative.mli | 25 ++++++++++++++++++ 2 files changed, 50 insertions(+), 1 deletion(-) diff --git a/helm/software/components/tactics/declarative.ml b/helm/software/components/tactics/declarative.ml index c22d51af2..a1c8cab69 100644 --- a/helm/software/components/tactics/declarative.ml +++ b/helm/software/components/tactics/declarative.ml @@ -1,3 +1,28 @@ +(* Copyright (C) 2006, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + let assume id t = Tacticals.then_ ~start: @@ -29,7 +54,6 @@ let by_term_we_proved t ty id = let bydone t = (Tactics.apply ~term:t) - ;; let we_need_to_prove t id = diff --git a/helm/software/components/tactics/declarative.mli b/helm/software/components/tactics/declarative.mli index b745ef5a1..2e9d506ca 100644 --- a/helm/software/components/tactics/declarative.mli +++ b/helm/software/components/tactics/declarative.mli @@ -1,3 +1,28 @@ +(* Copyright (C) 2006, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + val assume : string -> Cic.term -> ProofEngineTypes.tactic val suppose : Cic.term -> string -> ProofEngineTypes.tactic val by_term_we_proved : Cic.term -> Cic.term -> string -> ProofEngineTypes.tactic -- 2.39.2