From 9e28c50232e56e35437afb468c6d273abcf5eab5 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Wed, 1 Dec 2010 11:53:25 +0100
Subject: Imported Upstream version 0.2

---
 coq.mli | 117 ----------------------------------------------------------------
 1 file changed, 117 deletions(-)
 delete mode 100644 coq.mli

(limited to 'coq.mli')

diff --git a/coq.mli b/coq.mli
deleted file mode 100644
index 588a922..0000000
--- a/coq.mli
+++ /dev/null
@@ -1,117 +0,0 @@
-(***************************************************************************)
-(*  This is part of aac_tactics, it is distributed under the terms of the  *)
-(*         GNU Lesser General Public License version 3                     *)
-(*              (see file LICENSE for more details)                        *)
-(*                                                                         *)
-(*       Copyright 2009-2010: Thomas Braibant, Damien Pous.                *)
-(***************************************************************************)
-
-(** Interface with Coq where we import several definitions from Coq's
-    standard library. 
-
-    This general purpose library could be reused by other plugins.
-    
-    Some salient points:
-    - we use Caml's module system to mimic Coq's one, and avoid cluttering
-    the namespace;
-    - we also provide several handlers for standard coq tactics, in
-    order to provide a unified setting (we replace functions that
-    modify the evar_map by functions that operate on the whole
-    goal, and repack the modified evar_map with it).
-
-*)
-
-(** {2 Getting Coq terms from the environment}  *)
-
-val init_constant : string list -> string -> Term.constr
-
-(** {2 General purpose functions} *)
-
-type goal_sigma =  Proof_type.goal Tacmach.sigma 
-val goal_update : goal_sigma -> Evd.evar_map -> goal_sigma
-val resolve_one_typeclass : Proof_type.goal Tacmach.sigma -> Term.types -> Term.constr * goal_sigma
-val nf_evar : goal_sigma -> Term.constr -> Term.constr
-val evar_unit :goal_sigma ->Term.constr*Term.constr->  Term.constr* goal_sigma
-val evar_binary: goal_sigma -> Term.constr*Term.constr -> Term.constr* goal_sigma 
-
-
-(** [mk_letin name v] binds the constr [v] using a letin tactic  *)
-val mk_letin : string  ->Term.constr ->Term.constr * Proof_type.tactic 
-
-(** [mk_letin' name v] is a drop-in replacement for [mk_letin' name v]
-    that does not make a binding (useful to test whether using lets is
-    efficient) *)
-val mk_letin' : string  ->Term.constr ->Term.constr * Proof_type.tactic 
-
-(* decomp_term :  constr -> (constr, types) kind_of_term *)
-val decomp_term : Term.constr -> (Term.constr , Term.types) Term.kind_of_term
-
-
-(** {2 Bindings with Coq' Standard Library}  *)
-
-(** Coq lists *)
-module List:
-sig
-  (** [of_list ty l]  *)
-  val of_list:Term.constr ->Term.constr list ->Term.constr
-    
-  (** [type_of_list ty] *)
-  val type_of_list:Term.constr ->Term.constr
-end
-
-(** Coq pairs *)
-module Pair:
-sig
-  val typ:Term.constr lazy_t
-  val pair:Term.constr lazy_t
-end
-
-(** Coq positive numbers (pos) *)
-module Pos:
-sig
-  val typ:Term.constr lazy_t
-  val of_int: int ->Term.constr
-end
-
-(** Coq unary numbers (peano) *)
-module Nat:
-sig
-  val typ:Term.constr lazy_t
-  val of_int: int ->Term.constr
-end
-
-
-(** Coq typeclasses *)
-module Classes:
-sig
-  val mk_morphism: Term.constr -> Term.constr -> Term.constr -> Term.constr
-  val mk_equivalence: Term.constr ->  Term.constr -> Term.constr
-end 
-
-(** Both in OCaml and Coq, we represent finite multisets using
-    weighted lists ([('a*int) list]), see {!Matcher.mset}.
-
-    [mk_mset ty l] constructs a Coq multiset from an OCaml multiset
-    [l] of Coq terms of type [ty] *)
-
-val mk_mset:Term.constr -> (Term.constr * int) list ->Term.constr
-
-(** pairs [(x,r)] such that [r: Relation x]  *)
-type reltype = Term.constr * Term.constr
-
-(** triples [((x,r),e)] such that [e : @Equivalence x r]*)
-type eqtype = reltype * Term.constr
-
-
-(** {2 Some tacticials}  *)
-
-(** time the execution of a tactic *)
-val tclTIME : string -> Proof_type.tactic -> Proof_type.tactic
-
-(** emit debug messages to see which tactics are failing *)
-val tclDEBUG : string -> Proof_type.tactic -> Proof_type.tactic
-
-(** print the current goal *)
-val tclPRINT : Proof_type.tactic -> Proof_type.tactic
-
-
-- 
cgit v1.2.3